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

[Nils Anders Danielsson]

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.

-- 
/NAD