Idris 1.3.0 released

A new version of Idris, 1.3.0, has been released. You can find this on hackage, or from the download page. Documentation is available from This version primarily includes bug fixes and performance improvements – other changes since version 1.2.0 are detailed below.

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.

Language updates

  • Old induction tactics and eliminator generation functionality (%elim, %case, elim_for) is no longer supported. Please use the ones provided by Pruviloj and elaborator reflection instead.

Library updates

  • Changed rndInt in Effect.Random so that it does not alternate between odd and even.
  • Additions to contrib:
    • Data.SortedBag: Bag (or Multiset) implemention based on Data.SortedMap.
    • Data.PosNat: A Nat paired with a proof that it is positive.
    • Data.Chain: A function with an arbitrary number of arguments, plus combinators for working with them.

Tool updates

  • Added a switch --allow-capitalized-pattern-variables to optionally allow capitalized pattern variables after they were prohibited in 1.2.0.
  • REPL now prints an error message if program compiled by :exec terminates abnormally.
  • Idris now builds with GHC 8.4.
  • In the C backend, the representation of Idris values at runtime has been reworked.