coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strictly positive mutual inductive types

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strictly positive mutual inductive types
Date: Wed, 28 Feb 2018 11:38:12 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 6.mo173.mail-out.ovh.net
Ironport-phdr: 9a23:JkqmvR/RxdR+nv9uRHKM819IXTAuvvDOBiVQ1KB40uIcTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LWbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUIFeUAMudYr4zjqFAToxW5Hw+sA/r0yjRVgXL22Lc10+UlEQzd2QwvBd0PsHXRrNrrKagdT+a1w7fTzTnZYfNWwy7w5Y7VeR4iufGBRb19fMvLxUUyCw/Ijk+cpIPrMj+P0ukAvXCX4/duWO+skWIqrwB8riKxysswloXFnJ8Zx1PC+C5k2og6P8e4R1R+YdO8EJtfqSWaN4xuT84jWW1ovSE6xqAEtJO1ZiQKzY4oxx/ba/CedIiI/w7jWPyWITdmhHJpYrS/iAiu8US4y+38UNe70EpSoydKk9TArG0B2wDT58SdRfZw8F2t1DKB2gzL7+FLO0E0la7VK547xb4wk4IesUHZES/3nEX7l6qWeV8r++ip7uTofKjpqYGaN4BqkQHyKKoumtanDeQiLgcOR3Sb+fi71LD74UL5R6xKguQqnandrZDVPt8WprW5Ag9QyoYs8QyzDzag0NQCnHkINkhJeBydj9uhB1abK/fhSPy7nl6EkTFxxvmAMKeyLI/KKy3mmafgeLs1x89aSBF7mdVW5pZ8D7gRIff+VkL3uceeAAVvYF/8+PruFNgojtBWYmmIGKLMaPqD42/N3fomJqy3XKFQvT/8L/Y/4Pu30y08kE8ceKSl0J0acza2BKY/ehnLUT/Xmt4EVFwykE8mVuWz1g+HWC5SYnu+UqQx/Xc1EtD+VNqRdsWWmLWEmRyDMNhWa2RBUA7eTzHtcNzbALEJYSOWZ8h8jnoDS7jnTYI9h0mj

Hi,

What do you mean by "the theory of Containers"?

Maxime.

On 02/28/2018 11:28 AM, Matthieu Sozeau wrote:
> for example the theory of Containers justifies
> the construction of nested and mutual inductive types as far as I know.

[Coq-Club] Strictly positive mutual inductive types, Chantal Keller, 02/23/2018
- Re: [Coq-Club] Strictly positive mutual inductive types, Matthieu Sozeau, 02/28/2018
  - Re: [Coq-Club] Strictly positive mutual inductive types, Maxime Dénès, 02/28/2018
    - Re: [Coq-Club] Strictly positive mutual inductive types, Matthieu Sozeau, 02/28/2018