[Agda] Path to the standard library for the command line compiler

[José Pedro Magalhães]

Hello all,

I'm trying to compile an Agda file with the command line compiler. This
file uses the standard library, so I'm using the --include-path flag to
point to the location of the standard library:

agda --include-path="C:\agda2\lib-0.5\src" code.agda
>

But the compiler complains with:

The name of the top level module does not match the file name. The
> module code should be defined in one of the following files:
>   C:\agda2\lib-0.5\src\code.agda
>   C:\agda2\lib-0.5\src\code.lagda
>

Why is this? The file loads fine in emacs (with the agda2-include-dirs
Emacs mode variable set appropriately). This is with version 2.2.10, on
Windows.


Thanks,
Pedro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120111/1ecf9556/attachment.html