<div dir="ltr">Unless you have multiple Agda files needing different libraries in the same directory, the suggested way to do this is adding a .agda-lib file with a 'depend:' field to the directory (or a parent directory) containing the code.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Apr 20, 2016 at 3:11 PM, Harley Eades III <span dir="ltr"><<a href="mailto:harley.eades@gmail.com" target="_blank">harley.eades@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Hi, everyone.<span class=""><div><br><div><blockquote type="cite"><div>On Apr 20, 2016, at 5:14 AM, Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" target="_blank">Andrew.Pitts@cl.cam.ac.uk</a>> wrote:</div><br><div><div dir="ltr">On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>> wrote:<br>> Dear all,<br>><br>> The Agda Team is very pleased to announce the release of Agda 2.5.1.<br><br>I have a question about the new Library management features. <br><br>I would like to be able to specify which named library to use from within an .agda file. I hoped<br><br>{-# OPTIONS --library=foo #-}<br><br>would do it, but Agda says<br><br>Unrecognized option: --library=foo<br><br>so I guess this way of specifying a library is not possible — or did I get the syntax wrong?</div></div></blockquote><br></div></div></span><div>I was also hoping for this. Are there any plans to add it? It would simplify things a lot.</div><div><br></div><div>Best,</div><div>Harley</div></div><br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>