coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Indices in mutual inductives

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Indices in mutual inductives
Date: Fri, 5 Oct 2012 10:42:20 -0400

Dear list,

Coq rejects the following definition

Inductive A : B -> Type :=
| AIntro : forall b, A b

with B : Type :=
| BIntro : forall b (a : A b), B.

Is there any metatheoretical reason for this? Does anyone have an
example showing that it would make the logic inconsistent?

Thanks

--
Arthur Azevedo de Amorim

[Coq-Club] Indices in mutual inductives, Arthur Azevedo de Amorim, 10/05/2012
- Re: [Coq-Club] Indices in mutual inductives, Andreas Abel, 10/07/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Indices in mutual inductives, J. Ian Johnson, 10/05/2012
  - Re: [Coq-Club] Indices in mutual inductives, gallais @ ensl.org, 10/05/2012
- Re: [Coq-Club] Indices in mutual inductives, J. Ian Johnson, 10/05/2012
  - Re: [Coq-Club] Indices in mutual inductives, Arthur Azevedo de Amorim, 10/07/2012
    - Re: [Coq-Club] Indices in mutual inductives, J. Ian Johnson, 10/08/2012