[Agda] [ANNOUNCE] Agda 2.5.1

[Andrew Pitts]

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?

Thanks,

Andy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160420/9ba89069/attachment.html