1
------------------------------------------------------------------------
2
-- Release notes for Agda 2 version 2.2.6
3
------------------------------------------------------------------------
5
Important changes since 2.2.4:
10
* Universe polymorphism (experimental extension).
12
To enable universe polymorphism give the flag
13
--universe-polymorphism on the command line or (recommended) as an
16
When universe polymorphism is enabled Set takes an argument which is
17
the universe level. For instance, the type of universe polymorphic
20
id : {a : Level} {A : Set a} → A → A.
22
The type Level is isomorphic to the unary natural numbers and should be
23
specified using the BUILTINs LEVEL, LEVELZERO, and LEVELSUC:
25
data Level : Set where
29
{-# BUILTIN LEVEL Level #-}
30
{-# BUILTIN LEVELZERO zero #-}
31
{-# BUILTIN LEVELSUC suc #-}
33
There is an additional BUILTIN LEVELMAX for taking the maximum of two
36
max : Level → Level → Level
38
max (suc n) zero = suc n
39
max (suc n) (suc m) = suc (max n m)
41
{-# BUILTIN LEVELMAX max #-}
43
The non-polymorphic universe levels Set, Set₁ and so on are sugar
44
for Set zero, Set (suc zero), etc.
46
At present there is no automatic lifting of types from one level to
47
another. It can still be done (rather clumsily) by defining types
48
like the following one:
50
data Lifted {a} (A : Set a) : Set (suc a) where
53
However, it is likely that automatic lifting is introduced at some
56
* Multiple constructors, record fields, postulates or primitives can
57
be declared using a single type signature:
65
* Record fields can be implicit:
74
By default implicit fields are not printed.
76
* Record constructors can be defined:
78
record Σ (A : Set) (B : A → Set) : Set where
84
In this example _,_ gets the type
86
(proj₁ : A) → B proj₁ → Σ A B.
88
For implicit fields the corresponding constructor arguments become
91
Note that the constructor is defined in the /outer/ scope, so any
92
fixity declaration has to be given outside the record definition.
93
The constructor is not in scope inside the record module.
95
Note also that pattern matching for records has not been implemented
98
* BUILTIN hooks for equality.
102
data _≡_ {A : Set} (x : A) : A → Set where
105
can be specified as the builtin equality type using the following
108
{-# BUILTIN EQUALITY _≡_ #-}
109
{-# BUILTIN REFL refl #-}
111
The builtin equality is used for the new rewrite construct and
112
the primTrustMe primitive described below.
114
* New rewrite construct.
116
If eqn : a ≡ b, where _≡_ is the builtin equality (see above) you
119
f ps rewrite eqn = rhs
124
... | ._ | refl = rhs
126
The rewrite construct has the effect of rewriting the goal and the
127
context by the given equation (left to right).
129
You can rewrite using several equations (in sequence) by separating
130
them with vertical bars (|):
132
f ps rewrite eqn₁ | eqn₂ | … = rhs
134
It is also possible to add with clauses after rewriting:
136
f ps rewrite eqns with e
139
Note that pattern matching happens before rewriting—if you want to
140
rewrite and then do pattern matching you can use a with after the
143
See test/succeed/Rewrite.agda for some examples.
145
* A new primitive, primTrustMe, has been added:
147
primTrustMe : {A : Set} {x y : A} → x ≡ y
149
Here _≡_ is the builtin equality (see BUILTIN hooks for equality,
152
If x and y are definitionally equal, then
153
primTrustMe {x = x} {y = y} reduces to refl.
155
Note that the compiler replaces all uses of primTrustMe with the
156
REFL builtin, without any check for definitional equality. Incorrect
157
uses of primTrustMe can potentially lead to segfaults or similar
160
For an example of the use of primTrustMe, see Data.String in version
161
0.3 of the standard library, where it is used to implement decidable
162
equality on strings using the primitive boolean equality.
164
* Changes to the syntax and semantics of IMPORT pragmas, which are
165
used by the Haskell FFI. Such pragmas must now have the following
168
{-# IMPORT <module name> #-}
170
These pragmas are interpreted as /qualified/ imports, so Haskell
171
names need to be given qualified (unless they come from the Haskell
174
* The horizontal tab character (U+0009) is no longer treated as white
177
* Line pragmas are no longer supported.
179
* The --include-path flag can no longer be used as a pragma.
181
* The experimental and incomplete support for proof irrelevance has
187
* New "intro" command in the Emacs mode. When there is a canonical way
188
of building something of the goal type (for instance, if the goal
189
type is a pair), the goal can be refined in this way. The command
190
works for the following goal types:
192
- A data type where only one of its constructors can be used to
193
construct an element of the goal type. (For instance, if the
194
goal is a non-empty vector, a "cons" will be introduced.)
196
- A record type. A record value will be introduced. Implicit
197
fields will not be included unless showing of implicit arguments
200
- A function type. A lambda binding as many variables as possible
201
will be introduced. The variable names will be chosen from the
202
goal type if its normal form is a dependent function type,
203
otherwise they will be variations on "x". Implicit lambdas will
204
only be inserted if showing of implicit arguments is switched
207
This command can be invoked by using the refine command (C-c C-r)
208
when the goal is empty. (The old behaviour of the refine command in
209
this situation was to ask for an expression using the minibuffer.)
211
* The Emacs mode displays "Checked" in the mode line if the current
212
file type checked successfully without any warnings.
214
* If a file F is loaded, and this file defines the module M, it is an
215
error if F is not the file which defines M according to the include
218
Note that the command-line tool and the Emacs mode define the
219
meaning of relative include paths differently: the command-line tool
220
interprets them relative to the current working directory, whereas
221
the Emacs mode interprets them relative to the root directory of the
222
current project. (As an example, if the module A.B.C is loaded from
223
the file <some-path>/A/B/C.agda, then the root directory is
226
* It is an error if there are several files on the include path which
227
match a given module name.
229
* Interface files are relocatable. You can move around source trees as
230
long as the include path is updated in a corresponding way. Note
231
that a module M may be re-typechecked if its time stamp is strictly
232
newer than that of the corresponding interface file (M.agdai).
234
* Type-checking is no longer done when an up-to-date interface exists.
235
(Previously the initial module was always type-checked.)
237
* Syntax highlighting files for Emacs (.agda.el) are no longer used.
238
The --emacs flag has been removed. (Syntax highlighting information
239
is cached in the interface files.)
241
* The Agate and Alonzo compilers have been retired. The options
242
--agate, --alonzo and --malonzo have been removed.
244
* The default directory for MAlonzo output is the project's root
245
directory. The --malonzo-dir flag has been renamed to --compile-dir.
247
* Emacs mode: C-c C-x C-d no longer resets the type checking state.
248
C-c C-x C-r can be used for a more complete reset. C-c C-x C-s
249
(which used to reload the syntax highlighting information) has been
250
removed. C-c C-l can be used instead.
252
* The Emacs mode used to define some "abbrevs", unless the user
253
explicitly turned this feature off. The new default is /not/ to add
254
any abbrevs. The old default can be obtained by customising
255
agda2-mode-abbrevs-use-defaults (a customisation buffer can be
256
obtained by typing M-x customize-group agda2 RET after an Agda file
added
removed
doc/release-notes/2-2-6.txt
