[Agda] [ANNOUNCE] Agda 2.5.1

[Andrew Pitts]

I quote from Release notes for Agda version 2.5.1:

"The Agda.Builtin modules are installed in the same way as
Agda.Primitive, but unlike Agda.Primitive they are not loaded
automatically.”

This prompts me to ask a question that has bugged me for some time,
but not sufficiently to be bothered to ask this list, until now.

In what sense, exactly, is Agda.Primitive  “loaded automatically” ?
Naively, I would think the answer should be that the declarations in
Agda.Primitive are always available without having to say

open import Agda.Primitive

However, whereas

data foo  {ℓ }(A : Set ℓ) : Set ℓ where

typechecks OK,

data foo  {ℓ : Level}(A : Set ℓ) : Set ℓ where

does not (Agda complains that Level is not is scope), whereas

open import Agda.Primitive
data foo  {ℓ : Level}(A : Set ℓ) : Set ℓ where

does typecheck.

What am I mis-understanding here?

Andy


Andrew M. Pitts,
Professor of Theoretical Computer Science,
University of Cambridge Computer Laboratory,
William Gates Building, 15 JJ Thomson Ave,
Cambridge CB3 0FD, UK.

Tel +44 1223 334629,
Fax +44 1223 334678,
Email <Andrew.Pitts at cl.cam.ac.uk>,
Web   <www.cl.cam.ac.uk/users/amp12>.


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.
>
> GHC supported versions
> ======================
>
> Agda 2.5.1 has been tested with GHC 7.6.3, 7.8.4 and 7.10.3.
>
>
> Installation
> ============
>
>   cabal update && cabal install Agda
>
>
> Standard library
> ================
>
> The version of Agda standard library compatible with Agda 2.5.1 is
> available at
>
>   https://github.com/agda/agda-stdlib/releases/tag/v0.12
>
> (The release of the Agda standard library 0.12 will be announced
> later).
>
> What is new?
> ============
>
> In addition to the new features, changes, incompatibilities, fixed
> issues and enhancements announced on the release candidates 1 and 2
>
>   http://thread.gmane.org/gmane.comp.lang.agda/8378
>
>   http://thread.gmane.org/gmane.comp.lang.agda/8529
>
> the following issues were fixed:
>
> * https://github.com/agda/agda/issues/1796
>
> * https://github.com/agda/agda/issues/1821
>
> More information about the changes included in Agda 2.5.1 can be found
> in
>
>   http://hackage.haskell.org/package/Agda-2.5.1/changelog
>
>
> Enjoy Agda 2.5.1.
>
> --
> Andrés, on behalf of the Agda Team
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda