[Agda] [ANNOUNCE] Agda 2.5.1

[Andrés Sicard-Ramírez]

On 20 April 2016 at 04:14, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk> wrote:
> 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

Right. You cannot specify the library in this way.


-- 
Andrés