[Agda] [ANNOUNCE] Agda 2.5.1

[Andrew Pitts]

Andreas says

On 19 Apr 2016, at 10:49, Andreas Abel <abela at chalmers.se> wrote:

> Andy, Haskell is no better:
> ….
> With dependent types, you need to refer to things which are not in scope (unless you force the user to reimport recursively everything that is > mentioned in any imported type).
> Or what would be your suggestion?

and Thorsten says

> On 19 Apr 2016, at 11:14, Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk> wrote:
> Maybe I misunderstand you but it seems completely reasonable that you can
> define a module without opening it. You just need to use the qualified
> names instead of merging the name space. Not only Agda is doing this.

and Andy replies:

I don’t disagree with either of those comments. But what I meant is
that the few definitions in Agda.Primitive are so, well, primitive to
the rest of Agda, that I was expecting their names (Level, lzero, lsuc
and _⊔_) to be available to me automatically without having to
remember the incantation “open import Agda.Primitive”. But I can live
with it!

(The other issue is that despite some years using Agda, I had not got
my head around exactly where one can and where one cannot use “{arg}”
instead of “{arg:_}”.)

Andy