Idris 2 is a purely functional programming language with first class types.
For installation instructions, see INSTALL.md.
The wiki lists a number of useful resources, in particular
- What's changed since Idris 1
- Resources for learning Idris, including official talks that showcase its capabilities
- Editor support
The most common way to install the latest version of Idris and its packages is through pack Idris' package manager. Working with the latest version of Idris is as easy as pack switch latest.
Follow instructions on the pack repository for how to install pack.
To use pack and idris, you will need an .ipkg file (Idris-package file) that describes your idris project.
You can generate one with idris2 --init. Once setup with an .ipkg file, pack gives you access to the pack collection of packages, a set of compatible libraries in the ecosystem.
If your dependency is in the depends field of your .ipkg file, pack will automatically pull the dependency from you matching pack collection.
The wiki hosts a list of curated packages by the community.
Finally, pack also makes it easy to download, and keep updated version of, idris2-lsp, and other idris-related programs.
- Cumulativity (currently
Type : Type. Bear that in mind when you think you've proved something) rewritedoesn't yet work on dependent types
If you want to learn more about Idris, contributing to the compiler could be one way to do so. The contribution guidelines outline the process. Having read that, choose a good first issue or have a look at the contributions wanted for something more involved. This map should help you find your way around the source code. See the wiki page for more details.