The tutorial has also been updated.
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.
Idris is still research software, so we expect there to be bugs. Please don’t keep them to yourself! If you find any problem, please report it on the github issue tracker. It is very helpful if you can also provide a small test case which reproduces your problem.
Also, do let us know how you get on in general either via the mailing list or the #idris channel on irc.freenode.net.
The main new features and updates are:
- Inductive-inductive definitions are now supported (i.e. simultaneously defined types where one is indexed by the other)
- Implicits and type class constraints can now appear in scopes other than the top level
- Importing a module no longer means it is automatically reexported. A new
publicmodifier has been added to import statements, which will reexport the names exported from that module
@patterns. A pattern of the form
x@pon the left hand side matches
xin scope on the right hand side with value
Somoved out of prelude into base, in modules
- A new tactic
sourceLocationthat fills the current hole with the current source code span, if this information is available. If not, it raises an error
:aproposcommands can now be given optional package lists to search
- Modules can now have API documentation strings
Additionally, several long-standing issues have been resolved, particularly with pattern matching and coverage checking.