forked from idris-lang/Idris-dev
/
CHANGELOG
48 lines (37 loc) · 1.4 KB
/
CHANGELOG
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
New in 0.9.1:
-------------
User visible changes:
* DSL notation
* Record projection and update
* Totality checking and 'total' keyword
* Auto implicits and default argument values {auto n : T}, {default val n : T}
* Additions to prelude, including Nat and List theorems
* New libs: control.monad.identity, control.monad.state
Internal changes:
* Faster compilation (only compiling names which are used)
0.1.x to 0.9.0:
Complete rewrite. User visible changes:
* New proof/tactics syntax
* New syntax for pairs/dependent pairs
* Indentation-significant syntax
* Added type classes
* Added where clauses
* Added case expressions, pattern matching let and lambda
* Added monad comprehensions
* Added cumulativity and universe checking
* Ad-hoc name overloading
- Resolved by type or explicit namespace
* Modules (Haskell-style)
* public, abstract and private access to functions and types
* Separate type-checking
* Improved interactive environment
* Replaced 'do using' with Monad class
* Extended syntax macros
Internal changes:
* Everything :-)
* All definitions (functions, classes and instances) are elaborated to top
level, fully explicit, data declarations and pattern matching definitions,
which are verified by a minimal type checker.
This is the first release of a complete reimplementation. There will be bugs.
If you find any, please do not hesitate to contact Edwin Brady
(ecb10@st-andrews.ac.uk).