Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Non strictly positive occurrence in constructor

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Non strictly positive occurrence in constructor


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page