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.

-- 
/NAD