Stream: Coq users

Topic: Name term while in proof mode


view this post on Zulip GuiGeek (Dec 25 2023 at 11:51):

Hello everyone,
Merry christmas!

I would like to introduce a named function locally in a proof, so do something like let R := fun a b => f b = a right after intro f and then be able to use the Rsymbol.
Is this possible?

view this post on Zulip James Wood (Dec 25 2023 at 11:56):

I believe assert (R := fun a b => f b = a). is the way to do it. See https://coq.inria.fr/refman/proof-engine/tactics.html#controlling-the-proof-flow. I also use pose proof sometimes, too.

view this post on Zulip GuiGeek (Dec 25 2023 at 13:29):

Thanks a lot James pose (R := fun a b => f b = a). was the line I was looking for.


Last updated: Jun 18 2024 at 22:01 UTC