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

José Pedro Magalhães jpm at cs.uu.nl
Wed Jan 11 16:29:48 CET 2012

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

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

More information about the Agda mailing list