Hello all,<br><br>I&#39;m trying to compile an Agda file with the command line compiler. This file uses the standard library, so I&#39;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=&quot;C:\agda2\lib-0.5\src&quot; 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>