coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Andreas Abel <andreas.abel AT ifi.lmu.de>
- To: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Indices in mutual inductives
- Date: Sun, 07 Oct 2012 08:04:47 +0200
Agda accepts these types, but only in this declaration order:
mutual
data B : Set where
BIntro : forall b (a : A b) -> B
data A (b : B) : Set where
AIntro : A b
B has to be defined first to check the type signature of A : B -> Set.
I do not see a reason why this should be a source of inconsistency. Types like those are discussed in the work on "inductive-inductive definitions" by Anton Setzer, Frederic Forsberg et al.
On 05.10.12 4:42 PM, Arthur Azevedo de Amorim wrote:
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
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
- [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
- Re: [Coq-Club] Indices in mutual inductives, Arthur Azevedo de Amorim, 10/07/2012
Archive powered by MHonArc 2.6.18.