1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
|
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
```agda
open import M <using/hiding/renaming>
```
now translates to
```agda
import A
open A <using/hiding/renaming>
```
instead of
```agda
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:
```agda
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`.
|
