[Agda] built-in divMod

[Ulf Norell]

On Wed, Mar 20, 2019 at 9:37 PM Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> What built-ins is used in your Agda Prelude for efficient divMod ?
> Can you explain in simple words, what is the mathematical method?
> (it is difficult to understand the method just from the bare code).
>

I'm using the div-helper and mod-helper functions from Agda.Builtin.Nat. If
you look
at the code it contains an explanation of what they do. What makes it fast
is that these
functions are computed using Haskell integer div and mod for closed
numbers, but they
still have an Agda definition which makes it possible to prove properties
about them.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190322/dec8e5d5/attachment.html>