[Agda] how does BUILTIN work - practical programming in Agda

[Silvio Frischknecht]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

> could you please send me a self-contained version of this code
> (which compiles with Agda):

I'm not sure what you mean by self-contained. Do you mean without the
standard library. Anyway I appended a file that will compile with agda
2.3 and the current darcs standard library. And it takes about 30
seconds on my laptop and prints 1 to the console.

Silvio
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iQIcBAEBAgAGBQJO3BnTAAoJEDLsP+zrbatWCVIQANb0UsF6JPAzIynoF2ANLeL8
iwjt5mRcybnel2MjSxnlSZtsSjHkxH3RK1bfh+U179BD2a4LPRyXfS4lTs5LY3MJ
cd4OUignPH2i611HiSDV8KAceWA/xeyBr7HbLGQ5aEXWYLfE4J0S5emkyJo6BVjC
y0gVboZGffQbyUWiTshGAhOKsvIwHPFYT8+HFVRBfpK6HRRWKCEs2IVzM+XZY+Pt
gDNjPVLGOb6AAAoFAqz8Nh/rARgfT/lqn+UidWOxcCZLXlu+C8BHXjh2M7qnKB4t
pB1U8g7B5L3BceTsAklbrUzcoWWSklRLkSG1Adadf8lsgGrw5xVbL6eRvqkDjQPU
HSu0cMg7+clD1eH5c58e2GKvjpRzDqrjeFsDSRx9otU+RLUoUw2fXJ/yzOnlbzVV
4edWlvenKeRjkp9kX3AYm9kLeGXD9S5P0i+qkDgs0Y5JHIq3NH/8sCvCMTtfSegu
ERryol13f9Jk+ZUKDaf9ziFLTW6pdIP5MPtpuuA6xHc5mYsbHh0S2RNW1WrtfKWY
1yJUZUK7i69M5qHtNpL45+YDpFjbzfN59AN7lPsulhum1U7QIZqdOLrsDmxIDKfH
MJ+NyLV1ESmbsEyyKUVslFxwG48/JHOuBC2TBkSBev0H5LNmx3IcKLmFvqB5RIvo
SrR8mO0VZ2ZjQm49tv4w
=qFdp
-----END PGP SIGNATURE-----
-------------- next part --------------
module AgdaCount where

open import IO.Primitive using (IO; putStrLn)
open import Data.String using (toCostring)
open import Function
open import Data.Nat.Show using (show; showInBase)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)

num = 1000 * 1000 * 1000 ∸ 1000 * 1000 * 999 ∸ 1000 * 999 ∸ 999

main = putStrLn $ toCostring $ show num
-------------- next part --------------
A non-text attachment was scrubbed...
Name: AgdaCount.agda.sig
Type: application/octet-stream
Size: 543 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20111205/9c92607f/AgdaCount.agda.obj