Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Inductive Definitions and Positive Occurrences (again)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Inductive Definitions and Positive Occurrences (again)


chronological Thread 
  • From: Hermann Lehner <hermann.lehner AT inf.ethz.ch>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Inductive Definitions and Positive Occurrences (again)
  • Date: Fri, 22 Jan 2010 14:40:51 +0100

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



Archive powered by MhonArc 2.6.16.

Top of Page