coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strictly positive mutual inductive types
Date: Wed, 28 Feb 2018 10:49:48 +0000
Authentication-results: mail2-smtp-roc.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-f43.google.com
Ironport-phdr: 9a23:jbPORhMs9Tgj2LS9P/Al6mtUPXoX/o7sNwtQ0KIMzox0Lf/8rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoUIFeUBIfpYr4n8p1QQsBu1GBSiBOTuyzBWnHD2wLAx3uMkEQ7cwAwgA8gBsHHPodXwLqgSTfy1w7PNzTnZaPNWwzj95ZHOfxs8r/+MWrdwftDQyUkpDw7FiFKQqZD5Pz+PzOsCr3KX7/djVe+plmUpqBlxryCty8ojkIXFm5wZx1De+Sh63oo5P9K1RUB9bNW5CpVfrTuaOJFzQs46Q2FnpiI6yroetJ6+ZicKyZAnywfRavyCb4SE+xzjWemfLDtii3Jlf7W/hxm28Ue+0OHzSs600FNSoipElNnDqGwN2gTR58WIUPdx41mt1DaV2w3Q9O1IO085mKTDJ54k2LEwl54TsUrZHi/xnUX7lKqWeV84+ui06+TnY6vppoKGO49vjQH/M7ohldaiAekjPQgOWnKU+eW41LH54UL5R7BKguUskqbFqJDaOdgbpqmhDgBJ1YYj8g+zACui0NQFhnYKN0lFeRKCj4jxIV7COvH4DfGlg1Stijhn3f7GPqeySqnKe3PEifLqeat3w09a0gs6i95FtLxODbRUBfvvRk/wucGQNRgrPgWpi7LiAclh34Y2XGuTHqacdqTIvgnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCO10NgEGGYO+AE5Sb6z0QHQYXtof3+3GpkEyHQjEov/V9XGT5yxibnH2z20TMUPOzJ2T2uUGHKtTL2qHvcBbCXIf51kmz0AEKekE8oviUrouwj9xL5qaOHT/39AuA==

I'm refering for example to this paper:

http://www.cs.nott.ac.uk/~psztxa/publ/icalp04.pdf

-- Matthieu

On Wed, Feb 28, 2018 at 11:38 AM Maxime Dénès <mail AT maximedenes.fr> wrote:

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