coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Francois Pottier <Francois.Pottier AT inria.fr>
To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Eta-conversion in Coq 8.4 -- is there any documentation?
Date: Tue, 21 Feb 2012 13:29:37 +0100

On Tue, Feb 21, 2012 at 11:51:37AM +0100, Arnaud Spiwack wrote:
> The bottom line is that eta-expansion at the level of conversion is
> weaker than propositional extensionality.

Thanks, this is where I was confused.

--
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