@@ -22,6 +22,7 @@ New in 0.9.17:
2222* DSL notation can now be applied with $
2323* Added FFI_Export type which allows Idris functions to be exportoed and
2424 called from foreign code
25+* Instances can now have documentation strings.
2526
2627New in 0.9.16:
2728--------------
@@ -59,7 +60,7 @@ New in 0.9.15:
5960 solved automatically.
6061* More efficient representation of proof state, leading to faster elaboration
6162 of large expressions.
62−* EXPERIMENTAL Implementation of uniqueness types
63+* EXPERIMENTAL Implementation of uniqueness types
6364* Unary negation now desugars to "negate", which is a method of the Neg type class.
6465 This allows instances of Num that can't be negative, like Nat, and it makes correct
6566 IEEE Float operations easier to encode. Additionally, unary negation is now available
@@ -73,12 +74,12 @@ New in 0.9.15:
7374 library (see #1516)
7475* Terms in `code blocks` inside of documentation strings are now parsed and
7576 type checked. If this succeeds, they are rendered in full color in
76− documentation lookups, and with semantic highlighting for IDEs.
77+ documentation lookups, and with semantic highlighting for IDEs.
7778* Fenced code blocks in docs defined with the "example" attribute are rendered
7879 as code examples.
7980* Fenced code blocks declared to be Idris code that fail to parse or type check now
8081 provide error messages to IDE clients.
81−* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
82+* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
8283 Engine style)
8384
8485New in 0.9.14:
@@ -155,7 +156,7 @@ New in 0.9.12:
155156 ||| @ n the first number (examined by the function)
156157 ||| @ m the second number (not examined)
157158 plus (n, m : Nat) -> Nat
158−* Allow the auto-solve behaviour in the prover to be disabled, for easier
159+* Allow the auto-solve behaviour in the prover to be disabled, for easier
159160 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
160161* Updated 'effects' library
161162* New :apropos command at REPL to search documentation, names, and types
@@ -185,7 +186,7 @@ New in 0.9.11:
185186 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
186187 because the Vect constructors are defined in a namespace called Vect.
187188* assert_smaller internal function, which marks an expression as smaller than
188− a pattern for use in totality checking.
189+ a pattern for use in totality checking.
189190 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
190191 structurally smaller than "(x :: xs)"
191192* assert_total internal function, which marks a subexpression as assumed to
@@ -210,7 +211,7 @@ New in 0.9.10:
210211 types may now depend on earlier methods.
211212* More flexible class instance resolution, so that function types and lambda
212213 expressions can be made instances of a type class.
213−* Add !expr notation for implicit binding of intermediate results in
214+* Add !expr notation for implicit binding of intermediate results in
214215 monadic/do/etc expressions.
215216* Extend Effects package to cope with possibly failing operations, using
216217 "if_valid", "if_error", etc.
@@ -335,7 +336,7 @@ User visible changes:
335336Internal changes:
336337
337338* Separate inlining methods at compile-time and run-time
338−* Fixed nested parameters blocks
339+* Fixed nested parameters blocks
339340* Improve efficiency of elaborator by:
340341 - only normalising when necessary
341342 - reducing backtracking with resolving ambiguities
@@ -416,7 +417,7 @@ User visible changes:
416417Internal changes:
417418
418419* Some type class resolution fixes
419−* Several minor bug fixes
420+* Several minor bug fixes
420421* Performance improvements in resolving overloading and type classes
421422
422423New in 0.9.1:
@@ -464,11 +465,10 @@ Complete rewrite. User visible changes:
464465Internal changes:
465466
466467* Everything :-)
467−* All definitions (functions, classes and instances) are elaborated to top
468− level, fully explicit, data declarations and pattern matching definitions,
469− which are verified by a minimal type checker.
468+* All definitions (functions, classes and instances) are elaborated to top
469+ level, fully explicit, data declarations and pattern matching definitions,
470+ which are verified by a minimal type checker.
470471
471472This is the first release of a complete reimplementation. There will be bugs.
472−If you find any, please do not hesitate to contact Edwin Brady
473+If you find any, please do not hesitate to contact Edwin Brady
473474(ecb10@st-andrews.ac.uk).
474−