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
79
80
81
82
83
84
85
86
87
88
89
90
|
Release notes for Agda 2 version 2.4.0.2
========================================
* The Agda input mode now supports alphabetical super and subscripts,
in addition to the numerical ones that were already present.
[Issue [#1240](https://github.com/agda/agda/issues/1240)]
* New feature: Interactively split result.
Make case (`C-c C-c`) with no variables given tries to split on the
result to introduce projection patterns. The hole needs to be of
record type, of course.
```agda
test : {A B : Set} (a : A) (b : B) → A × B
test a b = ?
```
Result-splitting `?` will produce the new clauses:
```agda
proj₁ (test a b) = ?
proj₂ (test a b) = ?
```
If hole is of function type ending in a record type, the necessary
pattern variables will be introduced before the split. Thus, the
same result can be obtained by starting from:
```agda
test : {A B : Set} (a : A) (b : B) → A × B
test = ?
```
* The so far undocumented `ETA` pragma now throws an error if applied to
definitions that are not records.
`ETA` can be used to force eta-equality at recursive record types,
for which eta is not enabled automatically by Agda. Here is such an
example:
```agda
mutual
data Colist (A : Set) : Set where
[] : Colist A
_∷_ : A → ∞Colist A → Colist A
record ∞Colist (A : Set) : Set where
coinductive
constructor delay
field force : Colist A
open ∞Colist
{-# ETA ∞Colist #-}
test : {A : Set} (x : ∞Colist A) → x ≡ delay (force x)
test x = refl
```
Note: Unsafe use of `ETA` can make Agda loop, e.g. by triggering
infinite eta expansion!
* Bugs fixed (see [bug tracker](https://github.com/agda/agda/issues)):
[#1203](https://github.com/agda/agda/issues/1203)
[#1205](https://github.com/agda/agda/issues/1205)
[#1209](https://github.com/agda/agda/issues/1209)
[#1213](https://github.com/agda/agda/issues/1213)
[#1214](https://github.com/agda/agda/issues/1214)
[#1216](https://github.com/agda/agda/issues/1216)
[#1225](https://github.com/agda/agda/issues/1225)
[#1226](https://github.com/agda/agda/issues/1226)
[#1231](https://github.com/agda/agda/issues/1231)
[#1233](https://github.com/agda/agda/issues/1233)
[#1239](https://github.com/agda/agda/issues/1239)
[#1241](https://github.com/agda/agda/issues/1241)
[#1243](https://github.com/agda/agda/issues/1243)
|
