[Agda] Perplexed by compile behavior

[Nils Anders Danielsson]

On 2013-08-23 11:03, Chris Moline wrote:
> In emacs the file loads without error but when I try to compile it
> with the command line program I get this:

If you /load/ the program (C-c C-l), then it is not compiled, only
type-checked. You can also /compile/ using the Emacs mode (C-c C-x C-c).

> The type of main should be .IO.Primitive.IO A, for some A. The
> given type is .IO.IO .Data.Unit.

You can convert from IO.IO to IO.Primitive.IO by using IO.run.

-- 
/NAD