Create a definition using a proof script inside a proof script

In some proofs it might be necessary to define some constant using the proof mode. Which of the following variants would you prefer / find more elegant?

  • unshelve evar (y : nat).
  • unshelve refine (let x : nat := _ in _).
  • unshelve epose (z := _ : nat).
  • Other?

0 voters

The first two options result in the same proof term. The second option is a bit weird because evar is supposed to create a new evar, which is then immediatly unshelved.

In the last option, the new hypthesis will be z := (the_definition : nat) : nat, which is weird due to the redundant type casting.

IMO, the clearest syntax would be unshelve epose (z : nat := _).

I use a plain assert, usually, or unshelve evar if I need it to be transparent.


You can also use simple refine (let x : nat := _ in _). with a similar effect, no ?