coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with constructive rewriting

From: "John Wiegley" <johnw AT newartisans.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Problem with constructive rewriting
Date: Fri, 12 May 2017 13:36:40 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-pf0-f176.google.com
Ironport-phdr: 9a23:X8C5VBywzmPJOmnXCy+O+j09IxM/srCxBDY+r6Qd2+4TIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfWC5PDIO7bIUPAeQOMulEoIfyvFYOsQK+CBOwCO/z0DJFhHn71rA63eQ7FgHG2RQtE9wKvnTTrNX1MroZXuC0zKbWwjXDa+1Z2Dfz5IPVdR0ho/aMXbJ2ccvf0kQvER3Kj1uKpoz/IzOV1/8NvHKd7+p7T+6gl2knqwRorzWp28wihI7JhocPxVDF8yV02IA1KsO2SUFhe96kDJpQtzqAOItwWcMuWX1nuCE/yrAApJW1fzAKxYw5yxLDb/GLaYuF7xL5WOqMJTp0mmhpdK+9ihuz6UStyOzxWtOq3FtEoSdJiNjBu3QX2xDO5cWKTv1w9Vq71zmVzQDc8ORELFg0laXFL54hxaY9lp8JvkTCGi/6gV32jKGKekk99Oik9ubqb7T8qp+TMI90jQ7+MqAwlcClHes4NQ0OU3Ca+eS6yrLj4VX0TKtWgvAyiKXUs5DXKd4GqqO9HQNZyJsv5hS+Aju+1dQXh3gHLFZLeBKdiIjpPknDIPL2DPe+nVusnzNryO7GP7D6DZXNK2LMkLblfbpn90Fczw8zwchF551IErEBPO7zWkjpudPECR85KhW4zPrjCNVgzYwTQnmPA6+cMKPKq1CE/OMvI++WZI8UojnxMfYl5+S9xUM+zH0UZq6vlbQNb2ujVqBkKl6eZ3X2hcwaQE8FuwM/SKrhj1jUAhBJYHPnFYA75jdzN4OrAoPOV8rl1L6G3CGkNptbeWlcFlGXGHHzMY6DXqFfO2qpPsZ9n2lcBvCaQIg72ETr7Veixg==
Organization: New Artisans LLC

>>>>> "JG" == Jason Gross
>>>>> <jasongross9 AT gmail.com>
>>>>> writes:

JG> What happens if you Set Printing Universes? It sounds like this might be a
JG> bug...

The output then is:

Error: Illegal application:
The term "@flip@{Top.8173 Top.8174 Top.8175}" of type
"∀ (A : Type@{Top.8173}) (B : Type@{Top.8174}) (C : Type@{Top.8175}),
(A → B → C) → B → A → C"
cannot be applied to the terms
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}"
: "Type@{max(Coq.Classes.CEquivalence.6+1, Top.4+1)}"
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}"
: "Type@{max(Coq.Classes.CEquivalence.6+1, Top.4+1)}"
"Type@{Top.8172}" : "Type@{Top.8172+1}"
"arrow@{Top.8170 Top.8171}"
: "Type@{Top.8170} → Type@{Top.8171} → Type@{max(Top.8170, Top.8171)}"
The 4th term has type
"Type@{Top.8170} → Type@{Top.8171} → Type@{max(Top.8170, Top.8171)}"
which should be coercible to
"Type@{max(Coq.Classes.CEquivalence.6, Top.4)}
→ Type@{max(Coq.Classes.CEquivalence.6, Top.4)} → Type@{Top.8172}".

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
- <Possible follow-up(s)>
- [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
  - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
    - Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/12/2017
      - Re: [Coq-Club] Problem with constructive rewriting, Jason Gross, 05/12/2017
        
        Re: [Coq-Club] Problem with constructive rewriting, John Wiegley, 05/13/2017