The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Guillaume Allais wrote:
> The main difference is that assert do not provide you explicitly with the
> term you just constructed.
> I cannot see how to do this without proving a sublemma and finish its
> declaration by Defined instead of Qed and then use this sublemma in your
> developpement with the "pose (H := Mylemma)" feature.

I also have been trying to do that for a long time, but I did not manage
to create such a tactic. Actually, I was also going to make such a
request to coq-club.

I thought it could be possible mixing evar and refine yet I did not
succeeded because basically, the only way to may a cut is using cut or
assert, which only provide opaque inhabitants of a type. For example,

refine (let t := _ in _).

does not work as it does not provide the body of the term.

I would be happy if such a tactic existed, as this is very useful when
one wants to define in-proof terms through tactics.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature