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

* 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