The Coq mailing list

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

Thanks for your comments, Cedric and Damien.

It was indeed possible to use an inductive type instead of the fixpoint,
as you did in the example.

Greetings
Benedikt

Damien Pous wrote:
> Maybe you could replace the fixpoint with an inductive (I hope I
> didn't swap indices...) ?
> 
> Inductive vect X: nat -> Type :=
> | vnil: vect X O
> | vcons: forall n, X -> vect X n -> vect X (S n).
> 
> Inductive type: nat -> Type :=
>  | constr : forall n k, vect (type n) k -> type (S n).
> 
> Hope this helps,
> Damien
> 
> 
> 
> 2010/6/8 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
>>
>>
>>
>