@@ -20,6 +20,11 @@ New in 0.9.17:
20 an extra argument of type TTName. This allows more understandable
20 an extra argument of type TTName. This allows more understandable
21 dynamic errors in DSL code and more readable code generation results.
21 dynamic errors in DSL code and more readable code generation results.
22* DSL notation can now be applied with $
22* 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.
24New in 0.9.16:
29New in 0.9.16:
25--------------
30--------------
@@ -57,7 +62,7 @@ New in 0.9.15:
57 solved automatically.
62 solved automatically.
58* More efficient representation of proof state, leading to faster elaboration
63* More efficient representation of proof state, leading to faster elaboration
59 of large expressions.
64 of large expressions.
60−* EXPERIMENTAL Implementation of uniqueness types
65+* EXPERIMENTAL Implementation of uniqueness types
61* Unary negation now desugars to "negate", which is a method of the Neg type class.
66* Unary negation now desugars to "negate", which is a method of the Neg type class.
62 This allows instances of Num that can't be negative, like Nat, and it makes correct
67 This allows instances of Num that can't be negative, like Nat, and it makes correct
63 IEEE Float operations easier to encode. Additionally, unary negation is now available
68 IEEE Float operations easier to encode. Additionally, unary negation is now available
@@ -71,12 +76,12 @@ New in 0.9.15:
71 library (see #1516)
76 library (see #1516)
72* Terms in `code blocks` inside of documentation strings are now parsed and
77* Terms in `code blocks` inside of documentation strings are now parsed and
73 type checked. If this succeeds, they are rendered in full color in
78 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.
75* Fenced code blocks in docs defined with the "example" attribute are rendered
80* Fenced code blocks in docs defined with the "example" attribute are rendered
76 as code examples.
81 as code examples.
77* Fenced code blocks declared to be Idris code that fail to parse or type check now
82* Fenced code blocks declared to be Idris code that fail to parse or type check now
78 provide error messages to IDE clients.
83 provide error messages to IDE clients.
79−* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
84+* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient
80 Engine style)
85 Engine style)
82New in 0.9.14:
87New in 0.9.14:
@@ -153,7 +158,7 @@ New in 0.9.12:
153 ||| @ n the first number (examined by the function)
158 ||| @ n the first number (examined by the function)
154 ||| @ m the second number (not examined)
159 ||| @ m the second number (not examined)
155 plus (n, m : Nat) -> Nat
160 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
157 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
162 debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
158* Updated 'effects' library
163* Updated 'effects' library
159* New :apropos command at REPL to search documentation, names, and types
164* New :apropos command at REPL to search documentation, names, and types
@@ -183,7 +188,7 @@ New in 0.9.11:
183 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
188 write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
184 because the Vect constructors are defined in a namespace called Vect.
189 because the Vect constructors are defined in a namespace called Vect.
185* assert_smaller internal function, which marks an expression as smaller than
190* 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.
187 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
192 e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
188 structurally smaller than "(x :: xs)"
193 structurally smaller than "(x :: xs)"
189* assert_total internal function, which marks a subexpression as assumed to
194* assert_total internal function, which marks a subexpression as assumed to
@@ -208,7 +213,7 @@ New in 0.9.10:
208 types may now depend on earlier methods.
213 types may now depend on earlier methods.
209* More flexible class instance resolution, so that function types and lambda
214* More flexible class instance resolution, so that function types and lambda
210 expressions can be made instances of a type class.
215 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
212 monadic/do/etc expressions.
217 monadic/do/etc expressions.
213* Extend Effects package to cope with possibly failing operations, using
218* Extend Effects package to cope with possibly failing operations, using
214 "if_valid", "if_error", etc.
219 "if_valid", "if_error", etc.
@@ -333,7 +338,7 @@ User visible changes:
333Internal changes:
338Internal changes:
335* Separate inlining methods at compile-time and run-time
340* Separate inlining methods at compile-time and run-time
336−* Fixed nested parameters blocks
341+* Fixed nested parameters blocks
337* Improve efficiency of elaborator by:
342* Improve efficiency of elaborator by:
338 - only normalising when necessary
343 - only normalising when necessary
339 - reducing backtracking with resolving ambiguities
344 - reducing backtracking with resolving ambiguities
@@ -414,7 +419,7 @@ User visible changes:
414Internal changes:
419Internal changes:
416* Some type class resolution fixes
421* Some type class resolution fixes
417−* Several minor bug fixes
422+* Several minor bug fixes
418* Performance improvements in resolving overloading and type classes
423* Performance improvements in resolving overloading and type classes
420New in 0.9.1:
425New in 0.9.1:
@@ -462,11 +467,10 @@ Complete rewrite. User visible changes:
462Internal changes:
467Internal changes:
464* Everything :-)
469* Everything :-)
465−* All definitions (functions, classes and instances) are elaborated to top
470+* All definitions (functions, classes and instances) are elaborated to top
466− level, fully explicit, data declarations and pattern matching definitions,
471+ level, fully explicit, data declarations and pattern matching definitions,
467− which are verified by a minimal type checker.
472+ which are verified by a minimal type checker.
469This is the first release of a complete reimplementation. There will be bugs.
474This 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
471(ecb10@st-andrews.ac.uk).
476(ecb10@st-andrews.ac.uk).