Hi,<div><br></div><div>I've been trying to compile some agda programs from the terminal and stumbled upon some problems.</div><div><br></div><div>First I'm wondering what the point of the IO module is. The main-function seems to demand the IO "<a href="http://IO.Primitive.IO" target="_blank">IO.Primitive.IO</a>" and won't accept "<a href="http://IO.IO" target="_blank">IO.IO</a>".</div>
<div><br></div><div>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.</div>
<div><br></div><div>Anyway, once I replaced "<a href="http://IO.IO" target="_blank">IO.IO</a>" with "<a href="http://IO.Primitive.IO" target="_blank">IO.Primitive.IO</a>" and put my file in the standard lib folder everything worked out but I guess I shouldn't have to do either.</div>
<div><br></div><div>Finally I got a question regarding Nat. Will</div><div>> value100000 : Nat</div><div>> value100000 = 100000</div><div>be stored as</div><div>> suc (suc (suc (suc (suc (suc (suc (suc (.... 100000 times ...)</div>
<div>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</div>
<div>> test : Float</div><div>> test = 4.2</div><div>which seems to work (yay!) after I've defined "BUILTIN FLOAT Float" (but Data.Rational.\bq doesn't seem to use it)</div><div>)?</div><div><br></div>
<div>-- Oscar</div>