The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 09/05/2012 13:22, Robbert Krebbers a écrit :
> I am wondering why Coq does not allow the following inductive type.
> 
>   Inductive val : Type :=
>     | vnat : nat -> val
>     | varray (l : list val) : length l > 0 -> val.
> 
> It gives the following error
> 
>   Error: Non strictly positive occurrence of "val" in
>    "forall l : list val, length l > 0 -> val".
> 
> However, I do not see why the positivity condition does not hold.

"val" occurs (as an implicit argument) in "length l".


Cheers,

-- 
Stéphane