The tutorial has also been updated.
Thanks as always to everyone who has contributed, either with code, documentation or by testing and reporting issues. You can find the names of all contributors in the CONTRIBUTORS file in the source repository.
Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.
Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.
The main new features and updates are:
- Tactic for case analysis in proofs
- Induction and case tactic now work on expressions
- Support for running tests for a package with the tests section of
.ipkgfiles and the
- Clearly distinguish between type providers and postulate providers at the use site
- Allow dependent function syntax to be overridden in
dslblocks, similarly to functions and
let. The keyword for this is
effectslibrary, with simplified API
- Add support for
%libdirective for NodeJS
- Quasiquotes and quasiquote patterns allow easier work with reflected terms.
EXPR, causing the elaborator to be used to produce a reflected version of it. Subterms prefixed with
~are unquoted – on the RHS, they are reflected terms to splice in, while on the LHS they are patterns. A quasiquote expression can be given a goal type for the elaborator, which helps with disambiguation. For instance,
`(() : ())quotes the unit constructor, while
`(() : Type)quotes the unit type. Both goal types and quasiquote are typechecked in the global environment.
- Better inference of unbound implicits.