[Agda] is divMod slow?

[Sergei Meshveliani]

On Tue, 2017-06-20 at 12:53 +0200, Ulf Norell wrote:



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


How must it look the content of  ~/.agda/libraries  ?
(for example).


So far I use this:

       agda -c $agdaLibOpt ...

where the system variable  $agdaLibOpt  is set as 
 
  "-i . -i /home/mechvel/agda/stLib/apr13-2017/src     
   -i /home/mechvel/agda/UNPrelude/src 
   -i ...
  "
where UNPrelude is agda-prelude by Ulf Norell ("2.5.2-compatible").

Is this sufficient?


With this, the following test is not type-checked:

------------------------------------------------------
module UNPreludeTest where
open import Foreign.Haskell
open import IO.Primitive
open import Data.String using (String; toCostring)
open import Data.Nat.Show as NatShow 

open import Numeric.Nat.GCD using (gcd!)   -- of U. Norell

main : IO Unit
main = putStrLn (toCostring str) 
       where
       str = NatShow.show (gcd! 4 6)
------------------------------------------------------

  str = "abc"

also is not type-checked here.

The report of  Agda 2.6.0-207bde6  is

------------------------------
/home/mechvel/doconA/2.00/source/UNPreludeTest.agda:14,33-34
No instance of type
(.Agda.Builtin.FromNat.Number .Agda.Builtin.Nat.Nat) was found in
scope.
when checking that 4 is a valid argument to a function of type
({a : .Agda.Primitive.Level} {A : Set a}
 {{r : .Agda.Builtin.FromNat.Number A}} (n : .Agda.Builtin.Nat.Nat)
 {{_ : .Agda.Builtin.FromNat.Number.Constraint r n}} →
 A)
-------------------------------

Please, how to fix? 
Thanks,

------
Sergei