[Agda] original Nat
Ulf Norell
ulf.norell at gmail.com
Wed Dec 20 09:08:23 CET 2017
Natural number operations _are_ implemented in Agda, and you'll find the
definitions in
Agda.Builtin.Nat. The way that they are built in is that when called on
closed terms (for
instance 101 + 52), the type checker evaluates that using Haskell integer
arithmetic rather
than the Agda definitions.
You can read more here:
http://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers
Agda.Builtin.Nat is shipped with Agda. You can find its location either by
middle-clicking
the module name in Emacs, or by calling Agda from the command line with
`-v2`:
Bla.agda:
import Agda.Builtin.Nat
$ agda -v2 Bla.agda
Checking Bla (Bla.agda).
Loading Agda.Builtin.Bool
(/SOME_PATH/Agda-2.5.4/lib/prim/Agda/Builtin/Bool.agdai).
Loading Agda.Builtin.Nat
(/SOME_PATH/Agda-2.5.4/lib/prim/Agda/Builtin/Nat.agdai).
Finished Bla.
/ Ulf
On Tue, Dec 19, 2017 at 7:43 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:
> Please, what is a regular way to switch between the built-in Nat
> arithmetic and the original one (implemented in Agda) ?
>
> Data.Nat.Base of lib-0.14 contains
>
> open import Agda.Builtin.Nat public using ( zero; suc; _+_; _*_ )
> renaming ( Nat to ℕ; _-_ to _∸_ )
>
> But I do not find the module Agda.Builtin.Nat.
>
> I need to use the Nat arithmetic programmed in Agda
> (ℕ; _+_, _*_, _∸_, _≤_ ...) as in early days.
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20171220/aa7fdbe2/attachment.html>
More information about the Agda
mailing list