coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Cumulative inductive types and universe polymorphism

From: Matthieu Sozeau <mattam AT mattam.org>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Cumulative inductive types and universe polymorphism
Date: Mon, 07 Nov 2016 06:35:50 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f53.google.com
Ironport-phdr: 9a23:XkvuCBI3e78YBeTGEtmcpTZWNBhigK39O0sv0rFitYgULPnxwZ3uMQTl6Ol3ixeRBMOAuqgC2rGd6f2+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9SU3p/8jb3ss7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgz8ry/TLHUAHHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jQyTIdH2TL0pEQ+l/apiVVe8jS4bKzc82GTeltB5ieRcuh339E83+JLdfIzAbKk2RajaZ95PADMZBss=

Hi David,

Yes, we're planning to work on it with Amin Timany for 8.7 or the following version.
Do you have a particular application in mind?

Best,
-- Matthieu

On Sun, 6 Nov 2016 at 23:50, David Leduc <david.leduc6 AT googlemail.com> wrote:

Hello,

Universe polymorphism does not currently support cumulativity for
inductive types [1]. Is there any plan to add this feature in future
versions of Coq (8.6 or later)?

[1] Amin Timany, Bart Jacobs. First Steps Towards Cumulative Inductive
Types in CIC.
http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW684.abs.html

[Coq-Club] Cumulative inductive types and universe polymorphism, David Leduc, 11/06/2016
- Re: [Coq-Club] Cumulative inductive types and universe polymorphism, Matthieu Sozeau, 11/07/2016
  - Re: [Coq-Club] Cumulative inductive types and universe polymorphism, Bas Spitters, 11/07/2016