Releases: LeifW/Idris-dev
Releases · LeifW/Idris-dev
0.9.20.1
v0.9.19
New in 0.9.19: -------------- * The Idris Reference manual has been fleshed out with content originally found on the GitHub wiki. * The Show class has been moved into Prelude.Show and augmented with the method showPrec, which allows correct parenthesization of showed terms. This comes with the type Prec of precedences and a few helper functions. * New REPL command :printerdepth that 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 :printerdepth with no argument. * Compiler output shows applications of >>= in do-notation * fromInteger i where i is an integer constant is now shown just as i in compiler output * An interactive shell, similar to the prover, for running reflected elaborator actions. Access it with :elab from the REPL. * New command-line option --highlight that 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 ".idh". * Highlighting information is saved by the parser as well, allowing it to highlight keywords like "case", "of", "let", and "do" * Use predicates instead of boolean equality proofs as preconditions on List functions * More flexible 'case' construct, 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. * Some improvements in interactive editing, particularly in lifting out definitions and proof search. * Moved System.Interactive, along with getArgs to the Prelude. * Major improvements to reflected elaboration scripts, including the ability to run them in a declaration context and many bug fixes. * "decl syntax" rules to allow syntax extensions at the declaration level * Experimental Windows support for console colours