agda/doc/release-notes/2.2.4.md

Release notes for Agda 2 version 2.2.4

Important changes since 2.2.2:

• Change to the semantics of open import and open module. The declaration

  open import M <using/hiding/renaming>

now translates to

  import A
  open A <using/hiding/renaming>

instead of

  import A <using/hiding/renaming>
  open A

The same translation is used for open module M = E …. Declarations involving the keywords as or public are changed in a corresponding way (as always goes with import, and public always with open).

This change means that import directives do not affect the qualified names when open import/module is used. To get the old behaviour you can use the expanded version above.

• Names opened publicly in parameterised modules no longer inherit the module parameters. Example:

  module A where
    postulate X : Set

  module B (Y : Set) where
    open A public

In Agda 2.2.2 B.X has type (Y : Set) → Set, whereas in Agda 2.2.4 B.X has type Set.

• Previously it was not possible to export a given constructor name through two different open public statements in the same module. This is now possible.

• Unicode subscript digits are now allowed for the hierarchy of universes (Set₀, Set₁, …): Set₁ is equivalent to Set1.