[Agda] Re: Strict positivity and indices

[Nils Anders Danielsson]

On 2012-05-14 21:32, Andreas Abel wrote:
> For instance in
>
>    monus : Nat -> Nat -> Nat
>    monus zero y          = zero
>    monus (suc x) zero    = suc x
>    monus (suc x) (suc y) = monus x y
>
> are both arguments strictly positive?  And what does it mean then?

Agda states that the first argument is used strictly positively, and
that the other one is unused.

I don't know what this means (I didn't implement this feature, I only
optimised it).

-- 
/NAD