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

[Nils Anders Danielsson]

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 http://code.google.com/p/agda/issues/detail?id=172 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.

-- 
/NAD