coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?

From: Francois Pottier <Francois.Pottier AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?
Date: Tue, 21 Feb 2012 10:37:36 +0100

Dear all,

The list of changes for Coq 8.4 includes the addition of eta-conversion in
the logic. Is there any documentation that explains how this affects the
end user? What new possibilities are opened? For instance, does this mean
that the tactic "rewrite" can now be used under a lambda-abstraction? That
would be tremendously useful.

--
Fran�ois Pottier
Francois.Pottier AT inria.fr
http://gallium.inria.fr/~fpottier/

[Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?, Francois Pottier
- Re: [Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?, Arnaud Spiwack
- Message not available
  - Re: [Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?, Francois Pottier
- Re: [Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?, Tom Prince