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