Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Indices in mutual inductives

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Indices in mutual inductives


Chronological Thread 
  • 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/



Archive powered by MHonArc 2.6.18.

Top of Page