Idris 0.9.8 released

A new version of Idris, 0.9.8, has been released on hackage. The user visible changes are:

  • Added “rewrite … in …” construct
  • Allow type class constraints in ‘using’ clauses
  • Renamed EFF to EFFECT in Effect package
  • Experimental Java backend
  • Tab completion in REPL
  • Dynamic loading of C libraries in the interpreter
  • Testing IO actions at the REPL
  • Improve rendering of :t
  • Fixed some INTERNAL ERROR messages

Several internal changes have been made:

  • Fix non-linear pattern checking
  • Improved name disambiguation
  • More flexible unification and elaboration of lambdas
  • Various unification and totality checking bug fixes

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