@@ -20,6 +20,11 @@ New in 0.9.17:
2020 an extra argument of type TTName. This allows more understandable
2121 dynamic errors in DSL code and more readable code generation results.
2222* DSL notation can now be applied with $
23+* Effectful and IO function names for sending data to STDOUT have been
24+ aligned, semantically.
25+ + `print` is now for putting showable things to STDOUT.
26+ + `printLn` is for putting showable things to STDOUT with a new line
27+ + `putCharLn` for putting a single character to STDOUT, with a new line.
2328
2429New in 0.9.16:
2530--------------
@@ -57,7 +62,7 @@ New in 0.9.15:
5762 solved automatically.
5863* More efficient representation of proof state, leading to faster elaboration
5964 of large expressions.
60−* EXPERIMENTAL Implementation of uniqueness types
65+* EXPERIMENTAL Implementation of uniqueness types
6166* Unary negation now desugars to "negate", which is a method of the Neg type class.
6267 This allows instances of Num that can't be negative, like Nat, and it makes correct
6368 IEEE Float operations easier to encode. Additionally, unary negation is now available
@@ -71,12 +76,12 @@ New in 0.9.15:
7176 library (see #1516)
7277* Terms in `code blocks` inside of documentation strings are now parsed and
7378 type checked. If this succeeds, they are rendered in full color in
74− documentation lookups, and with semantic highlighting for IDEs.
79+ documentation lookups, and with semantic highlighting for IDEs.
7580* Fenced code blocks in docs defined with the "example" attribute are rendered
7681 as code examples.
7782* Fenced code blocks declared to be Idris code that fail to parse or type check now
7883 provide error messages to IDE clients.
79−* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
84+* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
8085 Engine style)
8186
8287New in 0.9.14:
@@ -153,7 +158,7 @@ New in 0.9.12:
153158 ||| @ n the first number (examined by the function)
154159 ||| @ m the second number (not examined)
155160 plus (n, m : Nat) -> Nat
156−* Allow the auto-solve behaviour in the prover to be disabled, for easier
161+* Allow the auto-solve behaviour in the prover to be disabled, for easier
157162 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
158163* Updated 'effects' library
159164* New :apropos command at REPL to search documentation, names, and types
@@ -183,7 +188,7 @@ New in 0.9.11:
183188 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
184189 because the Vect constructors are defined in a namespace called Vect.
185190* assert_smaller internal function, which marks an expression as smaller than
186− a pattern for use in totality checking.
191+ a pattern for use in totality checking.
187192 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
188193 structurally smaller than "(x :: xs)"
189194* assert_total internal function, which marks a subexpression as assumed to
@@ -208,7 +213,7 @@ New in 0.9.10:
208213 types may now depend on earlier methods.
209214* More flexible class instance resolution, so that function types and lambda
210215 expressions can be made instances of a type class.
211−* Add !expr notation for implicit binding of intermediate results in
216+* Add !expr notation for implicit binding of intermediate results in
212217 monadic/do/etc expressions.
213218* Extend Effects package to cope with possibly failing operations, using
214219 "if_valid", "if_error", etc.
@@ -333,7 +338,7 @@ User visible changes:
333338Internal changes:
334339
335340* Separate inlining methods at compile-time and run-time
336−* Fixed nested parameters blocks
341+* Fixed nested parameters blocks
337342* Improve efficiency of elaborator by:
338343 - only normalising when necessary
339344 - reducing backtracking with resolving ambiguities
@@ -414,7 +419,7 @@ User visible changes:
414419Internal changes:
415420
416421* Some type class resolution fixes
417−* Several minor bug fixes
422+* Several minor bug fixes
418423* Performance improvements in resolving overloading and type classes
419424
420425New in 0.9.1:
@@ -462,11 +467,10 @@ Complete rewrite. User visible changes:
462467Internal changes:
463468
464469* Everything :-)
465−* All definitions (functions, classes and instances) are elaborated to top
466− level, fully explicit, data declarations and pattern matching definitions,
467− which are verified by a minimal type checker.
470+* All definitions (functions, classes and instances) are elaborated to top
471+ level, fully explicit, data declarations and pattern matching definitions,
472+ which are verified by a minimal type checker.
468473
469474This is the first release of a complete reimplementation. There will be bugs.
470−If you find any, please do not hesitate to contact Edwin Brady
475+If you find any, please do not hesitate to contact Edwin Brady
471476(ecb10@st-andrews.ac.uk).
472−