coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Eta-expansion and simpl

From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Eta-expansion and simpl
Date: Fri, 16 Nov 2012 13:14:06 +0100

On 11/16/2012 01:08 PM, AUGER Cédric wrote:

What do you mean by 'eta-reduction' is unsound?

It makes confluence and subject reduction fail in the presence of subtyping. See slide 24 of http://pauillac.inria.fr/~herbelin/talks/cic.pdf. That is why Coq has (typed) eta-expansion instead.

Robbert

[Coq-Club] Eta-expansion and simpl, AUGER Cédric, 11/15/2012
- Re: [Coq-Club] Eta-expansion and simpl, Arnaud Spiwack, 11/16/2012
  - Re: [Coq-Club] Eta-expansion and simpl, AUGER Cédric, 11/16/2012
    - Re: [Coq-Club] Eta-expansion and simpl, Robbert Krebbers, 11/16/2012
      - Re: [Coq-Club] Eta-expansion and simpl, Arnaud Spiwack, 11/16/2012