2022-09-20 00:36:45 +03:00
# Idris 2
2020-05-18 16:03:28 +03:00
2020-05-20 17:19:27 +03:00
[![Documentation Status ](https://readthedocs.org/projects/idris2/badge/?version=latest )](https://idris2.readthedocs.io/en/latest/?badge=latest)
2023-10-04 12:28:47 +03:00
[![Build Status ](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2-and-libs.yml/badge.svg?branch=main )](https://github.com/idris-lang/Idris2/actions/workflows/ci-idris2-and-libs.yml?query=branch%3Amain)
2020-05-19 01:31:25 +03:00
2020-05-20 13:31:24 +03:00
[Idris 2 ](https://idris-lang.org/ ) is a purely functional programming language
with first class types.
2020-05-18 16:03:28 +03:00
2022-09-20 00:36:45 +03:00
For installation instructions, see [INSTALL.md ](INSTALL.md ).
2020-05-19 01:31:25 +03:00
2022-09-20 00:36:45 +03:00
The [wiki ](https://github.com/idris-lang/Idris2/wiki ) lists a number of useful resources, in particular
2020-05-20 13:31:24 +03:00
2022-09-20 00:36:45 +03:00
+ [What's changed since Idris 1 ](https://idris2.readthedocs.io/en/latest/updates/updates.html )
+ [Resources for learning Idris ](https://github.com/idris-lang/Idris2/wiki/Resources )
+ [Editor support ](https://github.com/idris-lang/Idris2/wiki/Editor-Support )
2020-05-20 13:31:24 +03:00
2022-09-20 00:36:45 +03:00
## Things still missing
2020-05-20 13:31:24 +03:00
2022-09-20 00:36:45 +03:00
+ Cumulativity (currently `Type : Type` . Bear that in mind when you think you've proved something)
+ `rewrite` doesn't yet work on dependent types
2020-05-20 13:31:24 +03:00
2022-09-20 00:36:45 +03:00
## Contributions wanted
2020-05-20 13:31:24 +03:00
2023-11-10 02:13:07 +03:00
If you want to learn more about Idris, contributing to the compiler could be one way to do so. The [contribution guidelines ](CONTRIBUTING.md ) outline the process. Having read that, choose a [good first issue][1] or have a look at the [contributions wanted][2] for something more involved. See [the wiki page][3] for more details.
[1]: < https: / / github . com / idris-lang / Idris2 / issues ? q = is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22 >
[2]: < https: / / github . com / idris-lang / Idris2 / wiki / What-Contributions-are-Needed >
[3]: < https: / / github . com / idris-lang / Idris2 / wiki / Getting-Started-with-Compiler-Development >