[Agda] main, IO, agda -c, Nat and Float

[Oscar Finnsson]

Hi,

I've been trying to compile some agda programs from the terminal and
stumbled upon some problems.

First I'm wondering what the point of the IO module is. The main-function
seems to demand the IO "IO.Primitive.IO" and won't accept "IO.IO".

Secondly I tried to put my file in a folder outside the standard library and
point to the standard lib using -i but then agda (the console application)
seems to demand that my module should be in the standard lib folder too.

Anyway, once I replaced "IO.IO" with "IO.Primitive.IO" and put my file in
the standard lib folder everything worked out but I guess I shouldn't have
to do either.

Finally I got a question regarding Nat. Will
> value100000 : Nat
> value100000 = 100000
be stored as
> suc (suc (suc (suc (suc (suc (suc (suc (.... 100000 times ...)
or will the compiler realise that it can just store 100000? If it realises
this: is it a general feature of all data types with similar definition as
Nat or it is special to Nat since it's builtin (btw, the source code
(Builtin.hs) mention a bunch of builtins. Is there any documentation over
what the different buildins stand for? Reading the source code I spotted a
Rational builtin which led me to test
> test : Float
> test = 4.2
which seems to work (yay!) after I've defined "BUILTIN FLOAT Float" (but
Data.Rational.\bq doesn't seem to use it)
)?

-- Oscar
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101016/2781f133/attachment.html