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

Nils Anders Danielsson nad at
Mon Apr 23 16:34:38 CEST 2012

On 2012-04-23 15:37, James Deikun wrote:
> The current stdlib implementation is clever, but thanks to depending
> on optimizations Agda still doesn't implement, it can take about 25
> seconds to reduce the product of two rationals (involving no more than
> 2-digit arithmetic).

I think you refer to the following comment:

   -- Note that Induction.Nat.<-rec is used to establish termination of
   -- division. The run-time complexity of this implementation of integer
   -- division should be linear in the size of the dividend, assuming
   -- that well-founded recursion and the equality type are optimised
   -- properly (see "Inductive Families Need Not Store Their Indices"
   -- (Brady, McBride, McKinna, TYPES 2003)).

Note that at least one of these optimisations (collapsing) is a
/run-time/ optimisation.


More information about the Agda mailing list