The Coq mailing list

[Freek Wiedijk <freek AT cs.kun.nl>]

Dear Hugo,

>More generally, do you mind a syntactic definition that
>hides the required proof of y#0 in the de def of "/" and add
>the proof obligation as a goal, possibly proving it
>automatically.

I wouldn't _mind_ that of course :-), but what I was thinking
of was something like having the possibility to write:

        (divide x y (LATEST y#0))

where "(LATEST T)" means the latest object of type T that has
been introduced (better syntax would be nice of course).  I
was talking about _expressions,_ not about tactics.

I mean, I want to be able to use these kind of expressions in
a Check etc., and in that case there certainly is not the
possibility to add proof obligations.  I even might not be
inside a goal when I do the Check: so there is not anything
like "proving" possible then.

Freek