New in 0.9.12:

--------------

* Proof search now works for metavariables in types, giving some interactive
  type inference.
* New 'Lazy' type, replacing laziness annotations.
* JavaScript and Node codegen now understand the %include directive.
* Concept of 'null' is now understood in the JavaScript and Node codegen.
* Lots of performance patches for generated JavaScript.
* New commands :eval (:e) and :type (:t) in the prover, which either normalise
  or show the type of expressions.
* Allow type providers to return postulates in addition to terms.
* Syntax for dealing with match failure in <- and pattern matching let.
* New syntax for inline documentation. Documentation starts with |||, and
  arguments are documented by preceding their name with @. Example:
  ||| Add two natural numbers
  ||| @ n the first number (examined by the function)
  ||| @ m the second number (not examined)
  plus (n, m : Nat) -> Nat
* Allow the auto-solve behaviour in the prover to be disabled, for easier
  debugging of proof automation. Use ":set autosolve" and ":unset autosolve".
* Updated 'effects' library
* New :apropos command at REPL to search documentation, names, and types
* Unification errors are now slightly more informative
* Support mixed induction/coinduction with 'Inf' type
* Add 'covering' function option, which checks whether a function and all
  descendants cover all possible inputs

Changes since previous version

------------------------------

* Agda-style equational reasoning (in Syntax.PreorderReasoning)
* 'case' construct now abstracts over the scrutinee in its type
* Added label type 'name (equivalent to the empty type).
  This is intended for field/effect disambiguation. "name" can be any
  valid identifier. Two labels are definitionally equal if they have the
  same name.
* General improvements in error messages, especially %error_reverse
  annotation, which allows a hint as to how to display a term in error
  messages
* --ideslave mode now transmits semantic information about many of the
  strings that it emits, which can be used by clients to implement
  semantic highlighting like that of the REPL. This has been implemented
  in the Emacs mode and the IRC bot, which can serve as examples.
* New expression form: with NAME EXPR privileges the namespace NAME
  when disambiguating overloaded names. For example, it is possible to
  write "with Vect [1,2,3]" at the REPL instead of "the (Vect _ _) [1,2,3]",
  because the Vect constructors are defined in a namespace called Vect.
* assert_smaller internal function, which marks an expression as smaller than
  a pattern for use in totality checking.
  e.g. "assert_smaller (x :: xs) (f xs)" asserts that "f xs" will always be
  structurally smaller than "(x :: xs)"
* assert_total internal function, which marks a subexpression as assumed to
  be total, e.g "assert_total (tail (x :: xs))".
* Terminal width is automatically detected if Idris is compiled with curses
  support. If curses is not available, automatic mode assumes 80 columns.
* Changed argument order for Prelude.Either.either.
* Experimental 'neweffects' library, intended to replace 'effects' in the
  next release.

Internal changes

* Faster elaboration
* Smaller .ibc files
* Pretty-printer now used for all term output

Hackage release 0.9.10

Changes since previous release:

* Type classes now implemented as dependent records, meaning that method
  types may now depend on earlier methods.
* More flexible class instance resolution, so that function types and lambda
  expressions can be made instances of a type class.
* Add !expr notation for implicit binding of intermediate results in
  monadic/do/etc expressions.
* Extend Effects package to cope with possibly failing operations, using
  "if_valid", "if_error", etc.
* At the REPL, "it" now refers to the previous expression.
* Semantic colouring at the REPL. Turn this off with --nocolour.
* Some prettifying of error messages.
* The contents of ~/.idris/repl/init are run at REPL start-up.
* The REPL stores a command history in ~/.idris/repl/history.
* The [a..b], [a,b..c], [a..], and [a,b..] syntax now pass the totality
  checker and can thus be used in types. The [x..] syntax now returns an
  actually infinite stream.
* Add '%reflection' option for functions, for compile-time operations on
  syntax.
* Add expression form 'quoteGoal x by p in e' which applies p to the expected
  expression type and binds the result to x in the scope e.
* Performance improvements in Strings library.
* Library reorganisation, separated into prelude/ and base/.

Internal changes

* New module/dependency tree checking.
* New parser implementation with more precise errors.
* Improved type class resolution.
* Compiling Nat via GMP integers.
* Performance improvements in elaboration.
* Improvements in termination checking.
* Various REPL commands to support interactive editing, and a client/server
  mode to allow external invocation of REPL commands.