Hello all,<br><br>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:<br><br>
<blockquote style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">agda --include-path="C:\agda2\lib-0.5\src" code.agda<br></blockquote><br>But the compiler complains with:<br>
<br><blockquote style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">The name of the top level module does not match the file name. The<br>module code should be defined in one of the following files:<br>
C:\agda2\lib-0.5\src\code.agda<br> C:\agda2\lib-0.5\src\code.lagda<br></blockquote><br>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.<br>
<br><br>Thanks,<br>Pedro<br>