<div dir="ltr"><div><div><font face="arial, helvetica, sans-serif">Natural number operations _are_ implemented in Agda, and you'll find the definitions in</font></div><div><font face="arial, helvetica, sans-serif">Agda.Builtin.Nat. The way that they are built in is that when called on closed terms (for</font></div></div><div><font face="arial, helvetica, sans-serif">instance 101 + 52), the type checker evaluates that using Haskell integer arithmetic rather</font></div><div><font face="arial, helvetica, sans-serif">than the Agda definitions.</font></div><div><br></div><div>You can read more here: <a href="http://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers">http://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers</a></div><div><br></div><font face="arial, helvetica, sans-serif">Agda.Builtin.Nat is shipped with Agda. You can find its location either by middle-clicking</font><div><font face="arial, helvetica, sans-serif">the module name in Emacs, or by calling Agda from the command line with `-v2`:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">Bla.agda:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif"> import Agda.Builtin.Nat<br></font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><font face="arial, helvetica, sans-serif">$ agda -v2 Bla.agda</font></div><div>
<p class="gmail-p1" style="margin:0px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;line-height:normal;color:rgb(0,0,0);background-color:rgb(255,255,255)"><font face="arial, helvetica, sans-serif"><span style="font-variant-ligatures:no-common-ligatures">Checking Bla (Bla.agda).</span><br></font></p>
<p class="gmail-p1" style="margin:0px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;line-height:normal;color:rgb(0,0,0);background-color:rgb(255,255,255)"><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures"><font face="arial, helvetica, sans-serif"><span class="gmail-Apple-converted-space"> </span>Loading<span class="gmail-Apple-converted-space"> </span>Agda.Builtin.Bool (/SOME_PATH/Agda-2.5.4/lib/prim/Agda/Builtin/Bool.agdai).</font></span></p>
<p class="gmail-p1" style="margin:0px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;line-height:normal;color:rgb(0,0,0);background-color:rgb(255,255,255)"><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures"><font face="arial, helvetica, sans-serif"><span class="gmail-Apple-converted-space"> </span>Loading<span class="gmail-Apple-converted-space"> </span>Agda.Builtin.Nat (/SOME_PATH/Agda-2.5.4/lib/prim/Agda/Builtin/Nat.agdai).</font></span></p>
<p class="gmail-p1" style="margin:0px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;line-height:normal;color:rgb(0,0,0);background-color:rgb(255,255,255)"><span class="gmail-s1" style="font-variant-ligatures:no-common-ligatures"><font face="arial, helvetica, sans-serif">Finished Bla.</font></span></p></div><div><br></div><div>/ Ulf</div><div><br></div><div class="gmail_extra"><div class="gmail_quote"><font face="arial, helvetica, sans-serif">On Tue, Dec 19, 2017 at 7:43 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br></font><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><font face="arial, helvetica, sans-serif">Please, what is a regular way to switch between the built-in Nat<br>
arithmetic and the original one (implemented in Agda) ?<br>
<br>
Data.Nat.Base of lib-0.14 contains<br>
<br>
open import Agda.Builtin.Nat public using ( zero; suc; _+_; _*_ )<br>
renaming ( Nat to ℕ; _-_ to _∸_ )<br>
<br>
But I do not find the module Agda.Builtin.Nat.<br>
<br>
I need to use the Nat arithmetic programmed in Agda<br>
(ℕ; _+_, _*_, _∸_, _≤_ ...) as in early days.<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
______________________________<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>
</font></blockquote></div><br></div></div>