coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Inductive Definitions and Positive Occurrences (again), Hermann Lehner
- RE: [Coq-Club] Inductive Definitions and Positive Occurrences, Lehner Hermann
Archive powered by MhonArc 2.6.16.