The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

You can use [set (a:= ....)].

V.



On Apr 6, 2010, at 6:25 AM, andré hirschowitz wrote:

> Hello world,
>
> How can I pose a local definition within a proof
>
> writing something like
> pose (myname := ? : mytype)
>  instead of
> pose (myname := myformula )
>
> in such a way that
> -the next goal becomes mytype
> -so that myformula can be generated in proof mode
> ?
>
> Thanks for your attention.
>
> ah