<div dir="ltr"><div><div>The divMod implementation of the standard library is also implemented using the  div-helper and mod-helper functions from Agda.Builtin.Nat. <br><a href="https://agda.github.io/agda-stdlib/Data.Nat.DivMod.html#4861">https://agda.github.io/agda-stdlib/Data.Nat.DivMod.html#4861</a><br><br></div>This makes me wonder in what way the prelude version differs from the standard library version.<br><br></div><div>Kind regards,<br></div><div>Jorn<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">2017-06-20 12:34 GMT+02:00 Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2017-06-20 at 12:04 +0200, Ulf Norell wrote:<br>
><br>
><br>
> On Tue, Jun 20, 2017 at 11:42 AM, Sergei Meshveliani<br>
> <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
><br>
>         1. What is a _regular_ way to download it? to use?<br>
><br>
<br>
> There are separate branches of the library for the different releases<br>
> of Agda (the master branch should work with the stable branch of<br>
> Agda). For instance, if you are using Agda-2.5.2 you should download<br>
> the compat-2.5.2 branch using the command<br>
><br>
>   git clone -b compat-2.5.2 <a href="https://github.com/UlfNorell/agda-prelude" rel="noreferrer" target="_blank">https://github.com/UlfNorell/<wbr>agda-prelude</a><br>
<br>
<br>
<br>
</span>I use  Agda 2.6.0-207bde6,<br>
<br>
and I recall that, probably, 2.5.2 is not sufficient for my code.<br>
<br>
Will  compat-2.5.2  work under  Agda 2.6.0-207bde6 ?<br>
<br>
And I need  gcd  on Nat  nearly as fast as in GHC on Integer.<br>
Or at least, a fast  divMod.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
<br>
<br>
> You should then add the path to agda-prelude.agda-lib to your<br>
> ~/.agda/libraries file (and optionally add agda-prelude to the<br>
> defaults file).<br>
><br>
><br>
> If you didn't add agda-prelude to the defaults file you need to add a<br>
> "depend" field to your project agda-lib file.<br>
><br>
><br>
><br>
>         Is  divMod  programmed there as built-in, or as an Agda<br>
>         program loop?<br>
><br>
><br>
> It's programmed using the div-helper and mod-helper functions from<br>
> Agda.Builtin.Nat. These are builtins which have an Agda definition but<br>
> are evaluated using primitive Haskell functions. See below.<br>
><br>
>         2. Another point.<br>
>         As I understand, the current Standard library implements  _+_<br>
>         and _*_ on<br>
>         Nat simply as built-in, with postulating certain main<br>
>         properties<br>
>         (may be, like this:  ∀ n -> suc-built-in n ≡ suc n).<br>
>         Right?<br>
><br>
><br>
> This is not how it works. _+_ and _*_ have Agda definitions (which you<br>
> can find in Agda.Builtin.Nat), so all desired properties can be proven<br>
> without postulates. However, when these functions are applied to<br>
> closed natural numbers (like 15 or 421783423) they are evaluated using<br>
> the corresponding primitive Haskell functions instead of the Agda<br>
> definitions.<br>
><br>
>         Is it difficult to apply the same approach to  divMod ?<br>
><br>
><br>
> This is exactly what agda-prelude does (applying the approach I<br>
> described above, that is).<br>
><br>
><br>
> / Ulf<br>
<br>
<br>
</div></div><div class="HOEnZb"><div class="h5">______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>