<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 20, 2019 at 9:37 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
What built-ins is used in your Agda Prelude for efficient divMod ?<br>
Can you explain in simple words, what is the mathematical method?<br>
(it is difficult to understand the method just from the bare code).<br></blockquote><div><br></div><div>I'm using the div-helper and mod-helper functions from Agda.Builtin.Nat. If you look</div><div>at the code it contains an explanation of what they do. What makes it fast is that these</div><div>functions are computed using Haskell integer div and mod for closed numbers, but they</div><div>still have an Agda definition which makes it possible to prove properties about them.</div><div><br></div><div>/ Ulf<br></div></div></div>