The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Well, this is just saying that B is empty. But it's usually ok to
define empty sets!

Inductive B : Set :=
  BIntro : B -> B.
Fixpoint omega (b : B) : False := match b with
  BIntro b' => omega b'
end.

--
gallais


On 5 October 2012 16:00, J. Ian Johnson 
<ianj AT ccs.neu.edu>
 wrote:
> 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