The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

Fixpoint omega (b : B) (a : A b) : False :=
 match a with
 | AIntro (BIntro b'' a') => omega b'' a'
 end.

----- Original Message -----
From: "Arthur Azevedo de Amorim" 
<arthur.aa AT gmail.com>
To: 
coq-club AT inria.fr
Sent: Friday, October 5, 2012 10:42:20 AM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] Indices in mutual inductives

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
| Base : forall 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