Stream: Coq users

Topic: Name term while in proof mode

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?

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.

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: Oct 13 2024 at 01:02 UTC