[Agda] [ANNOUNCE] Agda 2.5.1

[Harley Eades III]

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 <mailto: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160420/2a56a58a/attachment.html