Idris 0.9.9 released

A new version of Idris, 0.9.9, has been released on hackage. The tutorial has also been updated. The user visible changes are:

  • Apply functions by return type, rather than with arguments:
    • t <== f means "apply f with arguments such that it returns a value of type t"
  • Allow the result type of a rewrite to be specified:
    • rewrite prf ==> ty in val rewrites by prf, and checks that the resulting goal
      type is ty (Example)
  • Allow names to be attached to provisional definitions
    • lhs ?= {name} rhs generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional --- a unique name is generated if it is absent.
  • Experimental LLVM backend
  • Added Data.HVect module
  • Fix fromInteger to take an Integer, rather than an Int.
  • Integer literals for Fin n
  • Renamed O to Z, and fO to fZ to avoid confusion with the digit 0.
  • Swapped Vect arguments, now Vect : Nat -> Type -> Type
  • Added new DecEq instances
  • Add equiv tactic, which rewrites a goal to an equivalent (convertible) goal

Internal changes:

  • Add annotation for unification traces
  • Add mrefine tactic for refining by matching against a type
  • Type class resolution fixes
  • Much faster coverage checking

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