coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Freek Wiedijk <freek AT cs.kun.nl>
- To: coq-club AT pauillac.inria.fr
- Subject: Re: Feature request
- Date: Fri, 19 Nov 1999 11:55:12 +0100 (MET)
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
- Feature request, Freek Wiedijk
- Re: Feature request,
Hugo Herbelin
- Re: Feature request,
Freek Wiedijk
- Re: Feature request,
Jean-Christophe Filliatre
- Re: Feature request, Freek Wiedijk
- Re: Feature request,
Benjamin Werner
- Re: Feature request, Freek Wiedijk
- Re: Feature request, Pierre Courtieu
- Re: Feature request,
Benjamin Werner
- Re: Feature request, Freek Wiedijk
- Re: Feature request,
Jean-Christophe Filliatre
- Re: Feature request,
Freek Wiedijk
- Re: Feature request,
Hugo Herbelin
Archive powered by MhonArc 2.6.16.