coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat

From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat
Date: Wed, 6 Sep 2017 15:07:40 +0200

On 06/09/2017 13:58, Jacques-Henri Jourdan wrote:
> Also, more fundamentally, why doesn't that break subject reduction,
> given that eta-reduction is part of Coq's conversion rules?

This one is easy. Terms in Coq are only convertible up to eta-expansion,
not up to eta-reduction.

Best regards,

Guillaume

[Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/06/2017
- Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
  - Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
    - Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
      - Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
        
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
        
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
        
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/06/2017
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Guillaume Melquiond, 09/06/2017
        
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/06/2017
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/11/2017
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Matthieu Sozeau, 09/12/2017
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jacques-Henri Jourdan, 09/13/2017
        
        Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Ralf Jung, 09/14/2017
  - Re: [Coq-Club] Mysterious Universes introduced by List.tl and List.repeat, Jan-Oliver Kaiser, 09/06/2017