The Coq mailing list

[Robbert Krebbers <(e29315a54f%hidden_head%e29315a54f)mailinglists(e29315a54f%hidden_at%e29315a54f)robbertkrebbers.nl(e29315a54f%hidden_end%e29315a54f)>]

Hello Coq Club,

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.

Am I missing something, is the error message incorrect, or is this a bug?

Robbert