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

Ulf Norell ulf.norell at
Mon Apr 23 15:04:40 CEST 2012

On Mon, Apr 23, 2012 at 10:28 AM, Nils Anders Danielsson <nad at>wrote:

> 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**issues/detail?id=172<>for some context.

The purpose is to give you fast (=running on Haskell integers) div and mod
on nats
at compile time.

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.

The sanity checking for BUILTINs is supposed to disallow incorrect
if it doesn't it's a bug that should be fixed. The FFI and postulates
obviously let
you "prove" whatever you want, but BUILTINs shouldn't.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...

More information about the Agda mailing list