coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: ben <Benedikt.Ahrens AT unice.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Non strictly positive occurrence in constructor
- Date: Tue, 08 Jun 2010 13:29:26 +0200
Dear all,
I run into a "non strictly positive occurrence" in a situation which is
similar to the following simplified example:
============================
Fixpoint n_prod (X : Type) (n : nat) : Type :=
match n with
| O => unit
| S n => prod X (n_prod X n)
end.
Inductive type : nat -> Type :=
| constr : forall n k,
(n_prod (type n) k) -> type (S n).
============================
Is there an "equivalent definition" which would be accepted by Coq?
Thanks
Benedikt
- [Coq-Club] Non strictly positive occurrence in constructor, ben
Archive powered by MhonArc 2.6.16.