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.
caseconstruct, allowing each branch to target different types, provided that the case analysis does not affect the form of any variable used in the right hand side of the case.
decl syntaxrules to allow syntax extensions at the declaration level
- As usual, lots of improvements and fixes in elaboration
Showclass has been moved into
Prelude.Showand augmented with the method
showPrec, which allows correct parenthesisation of showed terms. This comes with the type
Precof precedences and a few helper functions.
Use predicates instead of boolean equality proofs as preconditions on
System.Interactive, along with
getArgsto the Prelude, in
New REPL command
:printerdepththat sets the pretty-printer to only descend to some particular depth when printing. The default is set to a high number to make it less dangerous to experiment with infinite structures. Infinite depth can be set by calling
:printerdepthwith no argument.
Compiler output shows applications of
iis an integer constant is now shown just as
iin compiler output
An interactive shell, similar to the prover, for running reflected elaborator actions. Access it with
:elabfrom the REPL.
- Major improvements to reflected elaboration scripts, including the ability to run them in a declaration context and many bug fixes.
- New command-line option
--highlightthat causes Idris to save highlighting information when successfully type checking. The information is in the same format sent by the IDE mode, and is saved in a file with the extension
- Highlighting information is saved by the parser as well, allowing it to highlight keywords like
- Some improvements in interactive editing, particularly in lifting out definitions and proof search. Proof search is now aware of type classes.
- Experimental Windows support for console colours.