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

Nils Anders Danielsson nad at
Mon Apr 23 10:28:58 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.

By the way, I'm not surprised that people manage to wreak havoc by using
BUILTINs, in many cases the sanity checking for BUILTINs is less than
optimal. I think the idea is that you should only use BUILTINs (and
postulates, and the FFI) if you know what you are doing.


More information about the Agda mailing list