[Agda] [ANNOUNCE] Agda 2.5.1

[Ulf Norell]

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.

/ Ulf

On Wed, Apr 20, 2016 at 3:11 PM, Harley Eades III <harley.eades at gmail.com>
wrote:

> Hi, everyone.
>
> On Apr 20, 2016, at 5:14 AM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
> wrote:
>
> On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> > Dear all,
> >
> > The Agda Team is very pleased to announce the release of Agda 2.5.1.
>
> I have a question about the new Library management features.
>
> I would like to be able to specify which named library to use from within
> an .agda file. I hoped
>
> {-# OPTIONS --library=foo #-}
>
> would do it, but Agda says
>
> Unrecognized option: --library=foo
>
> so I guess this way of specifying a library is not possible — or did I get
> the syntax wrong?
>
>
> I was also hoping for this.  Are there any plans to add it?  It would
> simplify things a lot.
>
> Best,
> Harley
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160420/e7c5805b/attachment.html