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

[Silvio Frischknecht]

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

> It does replace it with Haskell integers. The problem in this case
> is that the show function isn't built in, and the implementation in
> the standard library is very inefficient.
> 
> If you replace the right hand side of num by 1000, I suspect you
> would get the same behaviour.
> 
> / Ulf
> 

Yes i realised that too after I sent it. However, in my last response
to Andreas Abel I sent a similar program, which results in 1 and still
takes 30 seconds to calculate, and I am sure there it's not a problem
of the performance of show.

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

iQIcBAEBAgAGBQJO3IznAAoJEDLsP+zrbatWNhEP/2ADE5qUOsI+sb+mG0lAZG11
CmjkLEVVnwfQqz5NALGvBb6wAlI1YlTH0gWX7AfG1Su2nTZO2PFtSAjObz/oDQ0r
/NSdqoBnWHSoJ1RXQI+BKeEykIA/fileNMoEjihDw86r38RSA1HZxR6pcoO6322u
ch9FlmWnnaiX6WnTHM0VIQ2s9pQCpVqOD+O5KIPkYLbJ+ulPPSgx87Vqy4Sb1X98
VotuWp1JaHdzbFrfEywwmSWjpGAwzJQe4L/3YC6ZD/ysSnIrHsG2lu0bg2ChXDsI
I8+fs8QNRWXTrd/B0QGqA3KDIasu+vT9MzsCNhGs2o73r/JFuDTdnA1LF1pGV12J
FHEiYg68w7YpLmgX8aI0lrFum4ibqSXXUs6wpUoLQrve+vQleKAAIPkJq1XDvIrV
15IrS2Zn35cSakVM4DWxTfriEwIhpCJVgx8m672I0CE3Yyqo1dpp0O9ehgBp8GNY
/NjiofaVu7b3X/KpEiksQkXXmfnMsXSmhmpimMhmDXtFvtuyCKlSEOu2I7fnAsMl
ZW+h77qSu3rJOt4KImqUyTxp5CPhEXz1qCzhxiD9mgwJmPU9j9wFIm93JwApIJb5
iUkq+rOPK4/BOfqVCwpGHTae6YnwL+NwsG10OJAc3yDLOLQnYgivIStzwH+2M86n
m9IxZPOxeS+agMQQK2Xv
=wwUC
-----END PGP SIGNATURE-----