<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Jun 20, 2017 at 11:42 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="gmail-"><br>
</span>1. What is a _regular_ way to download it? to use?<br></blockquote><div><br></div><div>There are separate branches of the library for the different releases of Agda (the master branch should work with the stable branch of Agda). For instance, if you are using Agda-2.5.2 you should download the compat-2.5.2 branch using the command</div><div><br></div><div><font face="arial, helvetica, sans-serif">  <span style="font-variant-ligatures:no-common-ligatures">git clone -b compat-2.5.2 <a href="https://github.com/UlfNorell/agda-prelude">https://github.com/UlfNorell/agda-prelude</a></span></font></div>







<div> </div><div>You should then add the path to agda-prelude.agda-lib to your ~/.agda/libraries file (and optionally add agda-prelude to the defaults file).</div><div><br></div><div>If you didn't add agda-prelude to the defaults file you need to add a "depend" field to your project agda-lib file.</div><div><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>
Is  divMod  programmed there as built-in, or as an Agda program loop?<br></blockquote><div><br></div><div>It's programmed using the div-helper and mod-helper functions from Agda.Builtin.Nat. These are builtins which have an Agda definition but are evaluated using primitive Haskell functions. See below.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">2. Another point.<br>
As I understand, the current Standard library implements  _+_ and _*_ on<br>
Nat simply as built-in, with postulating certain main properties<br>
(may be, like this:  ∀ n -> suc-built-in n ≡ suc n).<br>
Right?<br></blockquote><div><br></div><div>This is not how it works. _+_ and _*_ have Agda definitions (which you can find in Agda.Builtin.Nat), so all desired properties can be proven without postulates. However, when these functions are applied to closed natural numbers (like 15 or 421783423) they are evaluated using the corresponding primitive Haskell functions instead of the Agda definitions.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Is it difficult to apply the same approach to  divMod ?<br></blockquote><div><br></div><div>This is exactly what agda-prelude does (applying the approach I described above, that is).</div><div><br></div><div>/ Ulf</div></div></div></div>