[Agda] is divMod slow?

[Ulf Norell]

On Tue, Jun 20, 2017 at 11:42 AM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> 1. What is a _regular_ way to download it? to use?
>

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

  git clone -b compat-2.5.2 https://github.com/UlfNorell/agda-prelude

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).

If you didn't add agda-prelude to the defaults file you need to add a
"depend" field to your project agda-lib file.


> Is  divMod  programmed there as built-in, or as an Agda program loop?
>

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.


> 2. Another point.
> As I understand, the current Standard library implements  _+_ and _*_ on
> Nat simply as built-in, with postulating certain main properties
> (may be, like this:  ∀ n -> suc-built-in n ≡ suc n).
> Right?
>

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.


> Is it difficult to apply the same approach to  divMod ?
>

This is exactly what agda-prelude does (applying the approach I described
above, that is).

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170620/87ddb601/attachment.html>