<div dir="ltr">No, include takes a path (corresponding to -i). In this case you want to depend on a named library, which is what the --library flag does.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Apr 20, 2016 at 5:50 PM, Andrew Pitts <span dir="ltr">&lt;<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" target="_blank">Andrew.Pitts@cl.cam.ac.uk</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 20 April 2016 at 14:48, Ulf Norell &lt;<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>&gt; wrote:<br>
&gt; Unless you have multiple Agda files needing different libraries in the same<br>
&gt; directory, the suggested way to do this is adding a .agda-lib file with a<br>
&gt; &#39;depend:&#39; field to the directory (or a parent directory) containing the<br>
&gt; code.<br>
<br>
</span>Don’t you mean an `include:’ field rather than a `depend:’ field?<br>
<br>
Andy<br>
</blockquote></div><br></div>