A new version of Idris, 1.1.0, has been released. You can find this on hackage, or from the download page. Documentation is available from
docs.idris-lang.org. Details of the changes since version 1.0 are listed 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.
contrib. These are small libraries for implementing total lexical analysers and parsers.
Text.PrettyPrint.WLan implementation of the Wadler-Leijen Pretty-Print algorithm.
- New instances:
- Added utility functions to
contrib), most notably
merge, merging two maps by their
Prelude.WellFoundednow contains an interface
Sized athat defines a size mapping from
Nat. For example, there is an implementation for lists, where
size = length.
sizeAccessiblethen proves well-foundedness of the relation
Smaller x y = LT (size x) (size y), which allows us to use strong induction conveniently with any type that implements
In practice, this allows us to write functions that recurse not only on direct subterms of their arguments but on any value with a (strictly) smaller
A good example of this idiom at work is
Added utility lemma
decEqSelfIsYes : decEq x x = Yes Reflto
Decidable.Equality. This is primarily useful for proving properties of functions defined with the help of
- Names are now annotated with their representations over the IDE protocol, which allows IDEs to provide commands that work on special names that don’t have syntax, such as case block names.