The Coq mailing list

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

Hi,

I don't think I asked this question yet:

A feature for Coq that I think might be useful is to have the
possibility to refer to the "last object introduced" of a
given type.  Both the "local" context as well as the sequence
of definitions and lemmas should be taken into account.

The application that I'm thinking of is of "hiding" the proof
objects needed to do division (that the denominator isn't
zero) inside a syntactic definition using this idiom.  Then
it would be possible to write something like x/y and it would
be legal when there is _some_ object of the type y#0 in
scope.

Is this a good idea?  An easy extension of the Coq syntax?
Or is this addition difficult?

Freek