[Agda] Re: Strict positivity and indices

[Stefan Monnier]

>> The Agda equivalent is:
>> 
>> data Val : Set where
>> nat : ℕ ->  Val
>> vec : (l : List Val) ->  0<  length l ->  Val
>> 
>> Coq rejects this as not being strictly positive. Agda doesn't complain.

> Agda remembers how the arguments to _<_ and length are used, and deduces
> that the definition is strictly positive.

Can you expand on how Agda does it?


        Stefan