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
91
92
93
94
95
96
97
98
99
100
101
102
|
Release notes for Agda 2 version 2.2.0
======================================
Important changes since 2.1.2 (which was released 2007-08-16):
Language
--------
* Exhaustive pattern checking. Agda complains if there are missing
clauses in a function definition.
* Coinductive types are supported. This feature is under
development/evaluation, and may change.
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.Codatatypes
* Another experimental feature: Sized types, which can make it easier
to explain why your code is terminating.
* Improved constraint solving for functions with constructor headed
right hand sides.
http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.FindingTheValuesOfImplicitArguments
* A simple, well-typed foreign function interface, which allows use of
Haskell functions in Agda code.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.FFI
* The tokens `forall`, `->` and `\` can be written as `∀`, `→` and
`λ`.
* Absurd lambdas: `λ ()` and `λ {}`.
http://thread.gmane.org/gmane.comp.lang.agda/440
* Record fields whose values can be inferred can be omitted.
* Agda complains if it spots an unreachable clause, or if a pattern
variable "shadows" a hidden constructor of matching type.
http://thread.gmane.org/gmane.comp.lang.agda/720
Tools
-----
* Case-split: The user interface can replace a pattern variable with
the corresponding constructor patterns. You get one new left-hand
side for every possible constructor.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode
* The MAlonzo compiler.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.MAlonzo
* A new Emacs input method, which contains bindings for many Unicode
symbols, is by default activated in the Emacs mode.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput
* Highlighted, hyperlinked HTML can be generated from Agda source
code.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.HowToGenerateWebPagesFromSourceCode
* The command-line interactive mode (`agda -I`) is no longer
supported, but should still work.
http://thread.gmane.org/gmane.comp.lang.agda/245
* Reload times when working on large projects are now considerably
better.
http://thread.gmane.org/gmane.comp.lang.agda/551
Libraries
---------
* A standard library is under development.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
Documentation
-------------
* The Agda wiki is better organised. It should be easier for a
newcomer to find relevant information now.
http://wiki.portal.chalmers.se/agda/
Infrastructure
--------------
* Easy-to-install packages for Windows and Debian/Ubuntu have been
prepared.
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download
* Agda 2.2.0 is available from Hackage.
http://hackage.haskell.org/
|
