Removal of NATxxxSUCAUX primitives [Re: [Agda] [BUG] builtins strike again -- Nat is a ring?]

Nils Anders Danielsson nad at
Mon Apr 23 10:25:50 CEST 2012

On 2012-04-23 09:07, Andreas Abel wrote:
> Mmh, the easiest fix is: trash the builtin NATDIVSUCAUX. I do not know what it is for. The only use I found for it was in
>   example/lib/Data/Nat.agda
> with the definition you have given below.

See for some context.


More information about the Agda mailing list