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 `R`

symbol.

Is this possible?

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.

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