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
publicare 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
moduleis 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
(Y : Set) → Set, whereas in Agda 2.2.4
- 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₁is equivalent to
Powered by PmWiki