The Coq mailing list

[Guillaume Allais <sbleune AT gmail.com>]

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.

--
gallais

On 6 April 2010 13:32, Stéphane Lescuyer <stephane.lescuyer AT inria.fr> wrote:

I don't see what is the problem with assert, "assert (H : P)" is
basically "cut P" with the goals generated the other way, so it is
exactly what you asked for in your first message ; in particular, it
does add an hypothesis named H of type P in the second goal.
Note that assert can be used as pose as well : "assert (H := t)" will
act as "pose (H := t); clearbody H".

HTH,

Stéphane

On Tue, Apr 6, 2010 at 1:22 PM, andré hirschowitz <ah AT unice.fr> wrote:
> no, if I experiment correctly.
>
> assert generates two goals and does not forward to the second one the
> formula produced for the first one.
>
> Thanks for your answer.
>
> ah
>
>>
>>
>> I think you are looking for the following?
>>
>>  assert (myname : mytype).
>>
>>
>
>

--
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06