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

Andreas Abel andreas.abel at
Mon Apr 23 20:54:14 CEST 2012

There are two issues with these built-ins:

1. I think they are unnecessary complicated due to the use of an 
accumulator argument to make them tail-recursive.  If internally we 
compute with the Haskell primitive, tail recursion does not give us 
anything besides complication.  I might be wrong here, so please 
contradict if it is the case.

2. They have an initial value m for a running parameter j, and the 
current proof of false exploits that that the running parameter j is 
initialized to a value above m, which violates an unspoken precondition 
of the functions.

If we are to keep these primitives, we need to extend their semantics to 
a j > m.  That should be easy.

But we should also consider removing the accumulator.  That would also 
simplify proofs about them.


On 23.04.12 3:04 PM, Ulf Norell wrote:
> On Mon, Apr 23, 2012 at 10:28 AM, Nils Anders Danielsson
> <nad at <mailto: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
>     <> 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
> definitions,
> 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

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at

More information about the Agda mailing list