[Agda] Strict positivity and indices

[Nils Anders Danielsson]

On 2012-05-09 18:37, Dan Doel wrote:
> 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.

Recently I discovered that the computation of this information can take
huge amounts of time. You can use -vtc.pos.graph:5 to see the sizes of
the positivity graphs that are constructed. The /transitive closures/ of
these graphs are used to find out how arguments are used.

I have optimised this machinery, so some code type-checks much faster
with the development version than with 2.3.0. However, these
computations can still be very time-consuming.

-- 
/NAD