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
docs.idris-lang.org. 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.
inductiontactics and eliminator generation functionality (
elim_for) is no longer supported. Please use the ones provided by
Pruvilojand elaborator reflection instead.
Effect.Randomso that it does not alternate between odd and even.
- Additions to
Data.SortedBag: Bag (or Multiset) implemention based on
Natpaired with a proof that it is positive.
Data.Chain: A function with an arbitrary number of arguments, plus combinators for working with them.
- Added a switch
--allow-capitalized-pattern-variablesto optionally allow capitalized pattern variables after they were prohibited in 1.2.0.
- REPL now prints an error message if program compiled by
- Idris now builds with GHC 8.4.
- In the C backend, the representation of Idris values at runtime has been reworked.