Idris 0.9.6 released

A new version of Idris, 0.9.6, has been released on hackage. This release has many updates and improvements. User visible changes are:

  • The type of types is now Type rather than Set
  • Forward declarations of data now allowed
    • supporting induction recursion and mutually recursive data
  • Type inference of definitions in where clauses
    • Provided that the type can be completely determined from the first
      application of the function (in the top level definition)
  • mutual blocks added
    • effect is to elaborate all types of declarations in the block before elaborating their definitions
    • allows inductive-recursive definitions
  • Expression inspected by with clause now abstracted from the goal (i.e. “magic” with)
  • Implicit arguments will be added automatically only if their initial letter is lower case, or they are in a using declaration
  • Added documentation comments (Haddock style) and :doc REPL command
  • Pattern matching on strings, big integers and characters
  • Added System.Concurrency modules
  • Added postulate declarations
  • Allow type annotations on let tactic
  • JavaScript generation, with --target javascript option

Internal changes:

  • Separate inlining methods at compile-time and run-time
  • Fixed nested parameters blocks
  • Improve efficiency of elaborator by:
    • only normalising when necessary
    • reducing backtracking with resolving ambiguities
  • Better compilation of case trees

Thanks to everyone who has helped put this release together.

As always, please report any problems on the github issue tracker. Also, do let us know how you get on in general either via the mailing list or the #idris channel on