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.