[Agda] Perplexed by compile behavior
Nils Anders Danielsson
nad at cse.gu.se
Fri Aug 23 15:32:30 CEST 2013
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.
More information about the Agda