The Coq mailing list

[ben <Benedikt.Ahrens AT unice.fr>]

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