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
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
Release notes for Agda version 2.4.2.5
======================================
Installation and infrastructure
-------------------------------
* Added support for GHC 7.10.3.
* Added `cpphs` Cabal flag
Turn on/off this flag to choose cpphs/cpp as the C preprocessor.
This flag is turn on by default.
(This flag was added in Agda 2.4.2.1 but it was not documented)
Pragmas and options
-------------------
* Termination pragmas are no longer allowed inside `where` clauses
[Issue [#1137](https://github.com/agda/agda/issues/1137)].
Type checking
-------------
* `with`-abstraction is more aggressive, abstracts also in types of
variables that are used in the `with`-expressions, unless they are
also used in the types of the
`with`-expressions. [Issue [#1692](https://github.com/agda/agda/issues/1692)]
Example:
```agda
test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
test f b with a | f b
test f b | .b | refl = f b
```
Previously, `with` would not abstract in types of variables that
appear in the `with`-expressions, in this case, both `f` and `b`,
leaving their types unchanged. Now, it tries to abstract in `f`, as
only `b` appears in the types of the `with`-expressions which are
`A` (of `a`) and `a ≡ b` (of `f b`). As a result, the type of `f`
changes to `(x : A) → b ≡ x` and the type of the goal to `b ≡ b` (as
previously).
This also affects `rewrite`, which is implemented in terms of
`with`.
```agda
test : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
test f b rewrite f b = f b
```
As the new `with` is not fully backwards-compatible, some parts of
your Agda developments using `with` or `rewrite` might need
maintenance.
Fixed issues
------------
See [bug tracker](https://github.com/agda/agda/issues)
[#1407](https://github.com/agda/agda/issues/1497)
[#1518](https://github.com/agda/agda/issues/1518)
[#1670](https://github.com/agda/agda/issues/1670)
[#1677](https://github.com/agda/agda/issues/1677)
[#1698](https://github.com/agda/agda/issues/1698)
[#1701](https://github.com/agda/agda/issues/1701)
[#1710](https://github.com/agda/agda/issues/1710)
[#1718](https://github.com/agda/agda/issues/1718)
|
