Idris 0.9.13 released

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

The tutorial has also been updated.

This release primarily improves robustness and efficiency, and more in-depth documentation. In particular, there is a new implementation of erasure by usage analysis.

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.

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

Aside from erasure, the new features and updates are:

  • New (first class) nested record update/access syntax:
    • record { a->b->c = val } x sets field accessed by c (b (a x)) to val
    • record { a->b->c } x accesses field, equivalent to c (b (a x))
  • IDE support for retrieving structured information about metavariables
  • Experimental Bits support for JavaScript
  • IdrisDoc: a Haddock- and JavaDoc-like HTML documentation generator
  • Command line option -e (or --eval) to evaluate expressions without loading the REPL. This is useful for writing more portable tests.
  • Many more of the basic functions and datatypes are documented
  • Primitive types such as Int and String are documented
  • Removed javascript lib in favor of idris-hackers/iQuery
  • Specify codegen for :compile REPL command (e.g. :compile javascript program.js)
  • Remove :info REPL command, subsume and enhance its functionality in the :doc command.
  • The banner at startup can be suppressed by adding :set nobanner to the initialisation script.
  • :apropos now accepts space-delimited lists of query items, and searches for the conjunction of its inputs. It also accepts binder syntax as search strings – for instance, -> finds functions.
  • Totality errors are now treated as warnings until code generation time, when they become errors again. This allows users to use the interactive editing features to fix totality issues, but no programs that violate the stated assumptions will actually run.
  • Added :makelemma command, which adds a new top level definition to solve a metavariable.
  • Extend :addclause to add instance bodies as well as definitions
  • Reverse parameters to BoundedList — now matches Vect, and is easier to instantiate classes.
  • Move foldl into Foldable so it can be overridden.
  • Experimental :search REPL command for finding functions by type