The Coq mailing list

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

Dear Jean-Christophe,

>If it is the case that the expected proof is the latest
>thing of that type introduced in the context,

In fact, _any_ object of that type would be fine AFAIC.
However, you want a syntactical construction to have a
definite meaning.

>But if we introduce a notation for ``the latest thing of
>type t'' then some users are going to require other
>notations for other objects of the context, other implicits
>proof terms, etc.

[grins]  I don't _require_ anything, I just thought it might
be a good idea :-)

>I definitively prefer to get a subgoal, even if it is a
>trivial one.

But, a subgoal is on the wrong level!  I'm talking about
expressions not about tactics!  I want to be able to write
x+y*z/w without mentioning proofs about w.  And I even want
to be able to write that where subgoals wouldn't make any
sense!

>I don't understand what would be the meaning of the last
>object of type T if you are not inside de goal.  If it is a
>constant c,

Yes, one of the parameters or constants.  You define "one",
you prove "one_ne_zero", and then everywhere you can write
"(LATEST one#0)" and it will mean that one_ne_zero.

>then you can give it directly, writing directly (divide x y
>c) instead of (divide x y (LATEST y#0)).

Yes, but the whole idea was to _hide_ the whole thing in
syntactic sugar!  I just want to write "(divide_abbrev x y)"
and not have to think all the time about what the name of the
proof object was.

Freek