The Coq mailing list

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

Randy wrote:

>When the Goal "xxx" is completly proved, the local
>definition "Fact3" becomes just that, a local "let" in the
>proof term.

I don't think Coq has "real" first-class local lets?  Coq's
lets are expanded at input time I guess?  Would it be hard to
add them to the system?  (Jean-Christophe?  Something for
your new kernel? :-))

"Lets" really make the expressive power of a single term much
more powerful.  I think.

Freek