Idris version 0.9.5 has been released on Hackage. To install, run
cabal update and type
cabal install idris. This release includes a new termination checker, coinduction, much improved compilation and code generation through more aggressive erasure and inlining, as well as several minor additions and fixes.
It includes the following user visible changes:
datadeclarations, but constructor arguments are evaluated lazily
- functions which return a
codatatype do not reduce at compile time
- New termination checker supporting mutually recursive definitions.
- Allow local data definitions in where blocks
%defaultdirective to declare total-by-default or partial-by-default for functions, and a corresponding
partialreserved word to mark functions which are allowed to be partial.
- Command line options
--partialto declare total or partial by default.
- Command line option
--warnpartialfor flagging all undeclared partial functions, without error.
:loadcommand to REPL, for loading a new file
:modulecommand to REPL, for adding modules
- Renamed library modules (now have initial capital)
The internal changes are:
- Added collapsing optimisation and more aggressive erasure
- Several improvements and fixes to unification
Thanks to everyone who has helped put this release together.