[Agda] [ANNOUNCE] Agda 2.5.1

[Andrew Pitts]

On 18 April 2016 at 18:07, Bradley Hardy <bch29 at cam.ac.uk> wrote:
> Hi Andy,
>
> I believe it’s the actual definitions of the primitive types and functions that are loaded automatically. The names are a separate matter. The automatic inference of types whose names aren’t in scope happens elsewhere too. If we have modules and definitions like so:
>…

Thanks for that explanation. I can’t say I find this aspect of Agda’s
behaviour desirable.

Andy