[Agda] Nat arithmetic properties

[Nils Anders Danielsson]

On 2016-09-21 15:26, Sergei Meshveliani wrote:
> And  Integer  is probably represented in GHC implementation as a list
> (array?) of macrodigits.

By default GHC uses a wrapper around GMP:

   https://hackage.haskell.org/package/integer-gmp-1.0.0.1/docs/src/GHC.Integer.Type.html

I think GHC makes use of GMP's low-level mpn_ functions:

   https://gmplib.org/manual/Low_002dlevel-Functions.html#Low_002dlevel-Functions

-- 
/NAD