The Coq mailing list

[Hermann Lehner <hermann.lehner AT inf.ethz.ch>]

Dear all,

There were already some discussions about similar issues, however, I 
can't explain the following.

I'm aware that the example doesn't make sense, but it shows the essence 
of a problem that i've got in a development of mine of a much larger scale.

(* The following doesn't work (Coq 8.2pl1) *)

Inductive i1 (t : Type) :=
     with i2 (t : Type) :=.
Inductive i3 :=
| def: i1 i3 -> i3.


Here, I get a "Non strictly positive occurence" Error.


The following similar constructs work fine, and I can't see the 
conceptual difference.

(* This works *)
Inductive i1 (t : Type) := .

Inductive i3 :=
| def: i1 i3 -> i3.


(* This works too *)
Inductive i1 :=
with      i2 :=
with      i3 :=
| d: i1 -> i3.



Anyone a clue? Thank!

Hermann

--
http://www.pm.inf.ethz.ch/people/lehnerh