Idris released

A new version of Idris,, has been released. You can find this on hackage, or from the
download page.

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)
  • 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 are:

  • Faster parsing and elaboration
  • Smaller .ibc files
  • 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