coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative Set

From: Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Impredicative Set
Date: Tue, 2 Apr 2019 16:53:00 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Thorsten.Altenkirch AT nottingham.ac.uk; spf=Pass smtp.mailfrom=Thorsten.Altenkirch AT nottingham.ac.uk; spf=None smtp.helo=postmaster AT uidappmx06.nottingham.ac.uk
Ironport-phdr: 9a23:1dRrMxKINyf+sACpy9mcpTZWNBhigK39O0sv0rFitYgfLP/xwZ3uMQTl6Ol3ixeRBMOHsqsC07Kd4/2oGTRZp8rY6DZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq9QajZF+JqotxRfEoXtFcPlSyW90OF6fhRnx6tqs8JJ57yhcp/ct/NNcXKvneKg1UaZWByk8PWAv483ruxjDTQ+R6XYZT24bjBlGDRXb4R/jRpv+vTf0ueR72CmBIM35Vqs0Vii476dqUxDnliEKPCMk/W7Ni8xwiKVboA+9pxF63oXZbp2ZOOZ4c6jAe94RWGhPUdtLVyFZAo2ycZYBD/YPM+hboYnypVUBrRqiCgejC+zi0SNIiWTz3aEmz+gsCwPL0Qo9FNwOqnTUq9D1Ob8MX+C1y6nI1y7Db+9I1jf79YPFbhQhoe2SUrJ2csrRyFMvGB/Fjl6NroHrITOV1uMXs2iA8+pvS+Svh3Q7pgF1vjig2MEsiorIhoIP1l/E9T50wIAyJd2kVE57YNikEJRQty6AMot6WNktTH1ytCYnyb0LoJi2dzUJxpQ/3xPTduKLfouS7h79W+ucLy10iX1rdb6lmhq+70ytxvXhWsWq01tGtDRJn9bCu3wXyRDf9tKLRuZy80u9wTqP2R7c5+JYLU0xkKfWJIMuzaQsmZcWr0vMBDH5lFnzgaKXdUgp+ual5uHob7Xou5OTK4l5gRzkPKs0gMywG+E4PxAOX2eF/eS806Xu/VD4QLpXlPI2irHZsJXVJMgHp6O1GQlV0oE/6xajDjem1tsYnXkdI1JAYh6IlZTmN0vTIPD7Ffu/glKsnyl3x/3eI7HtHJbAImLdnLruc7tx8UFRxQQpwdxC+Z5ZDqkNIPfpVU/wsNzYAAU5Mwuxw+v/Ftt91oQeWXiUAq+FLqzSt0WE6/4rI+mQeoAVvjX9K/k/5/HyjX80glkdfa613ZsLaXC4GPtmI0WDbnrpmNsOC3sFshAjTOzpkFGCSyJcZ26uX6Ig4TE2EJ6pDYDaRoy0nLOB2Dq7EYZNa2BdClGMFG/oeJ+eV/cNbiKSOM5hnSYeWbivUY9ynS2p4UXxzKMiJe7J8AUZs4ji3Z57/aebwRo17Hl/C9mX+2CLVWB92G0SEWwYxqd69HB9zU2YzaV+y9VcCdFV5PJTWQdyYaLcyPZhF930HCvFYtqPS1e8SdWOBzYtUtM3zN8HZgB0EJO/jUaQjGKRH7YJmunTV9QP+aXG0i2pfpcv+zP9zKAkymIebI5KPGyiiLR48lGDVYjOj1mYkamqfKFa1SWL6WTRlDPS7nEdaxZ5VOD+ZV5aflHf9ISr4ETeU76oBrQuN01IwoifKfkSM4C7vRB9XP7mfe/mTSexlmO3X0fa27KAZZLyfnVFgmPbD1QYkgYc/X+DcwE1QDqi8TrT

On 02/04/2019, 17:49,
"coq-club-request AT inria.fr
on behalf of Stefan Monnier"
<coq-club-request AT inria.fr
on behalf of
monnier AT IRO.UMontreal.CA>
wrote:

I think the more important aspect is that you can only erase terms which
are known to be pure (and hence terminating). For that reason Type:Type
makes erasure of type arguments more difficult.

That is a good point. To achieve this you don't have to work in a system
which is terminating but it is sufficient that the terms you need to erase
are terminating.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
- Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
  - Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
    - Re: [Coq-Club] Impredicative Set, Xavier Leroy, 04/02/2019
      - Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019
      - Re: [Coq-Club] Impredicative Set, Stefan Monnier, 04/02/2019
        
        Re: [Coq-Club] Impredicative Set, Thorsten Altenkirch, 04/02/2019