The tutorial has also been updated.
This release mostly improves robustness and efficiency. The user visible changes are:
- Agda-style equational reasoning (in Syntax.PreorderReasoning)
caseconstruct now abstracts over the scrutinee in its type
- Added label type
'name(equivalent to the empty type). This is intended for field/effect disambiguation.
namecan be any valid identifier. Two labels are definitionally equal if they have the same name.
- General improvements in error messages, especially
%error_reverseannotation, which allows a hint as to how to display a term in error messages
--ideslavemode 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
namewhen 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
Vectconstructors are defined in a namespace called
assert_smallerinternal 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 xswill always be structurally smaller than
(x :: xs).
assert_totalinternal 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
neweffectslibrary, intended to replace
effectsin the next release.
Internal changes are:
- Faster parsing and elaboration
- Pretty-printer now used for all term output
Thanks, as ever, to everyone who has helped put this release together. You can find their names in the CONTRIBUTORS file in the source repository.
Being research software, 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.