[Agda] Re: Strict positivity and indices

Nils Anders Danielsson nad at chalmers.se
Tue May 15 11:17:07 CEST 2012

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).


More information about the Agda mailing list