coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eta(?) conversion in records?

From: Adam Chlipala <adamc AT csail.mit.edu>
To: Matthieu Sozeau <mattam AT mattam.org>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] eta(?) conversion in records?
Date: Tue, 28 Aug 2012 08:28:49 -0400

On 08/28/2012 08:27 AM, Matthieu Sozeau wrote:

η for (non-recursive) records will come along with a more efficient
representation for projections which will not carry parameters anymore (as in
Agda too).

This sounds a little scary from a trusted-code-base-size perspective. Does the proof checker need to get more complex to support your addition?

[Coq-Club] eta(?) conversion in records?, Jason Gross, 08/18/2012
- Re: [Coq-Club] eta(?) conversion in records?, Andreas Abel, 08/27/2012
  - Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
    - Re: [Coq-Club] eta(?) conversion in records?, Adam Chlipala, 08/28/2012
      - Re: [Coq-Club] eta(?) conversion in records?, Matthieu Sozeau, 08/28/2012
        
        Re: [Coq-Club] eta(?) conversion in records?, Adam Chlipala, 08/28/2012
        
        Re: [Coq-Club] eta(?) conversion in records?, Ryan Wisnesky, 08/28/2012
        
        Re: [Coq-Club] eta(?) conversion in records?, Andrew Cave, 08/28/2012