2023-11-10 16:38:12 +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
|
|
|
|
2023-11-10 16:31:54 +03:00
|
|
|
[Idris 2](https://idris-lang.org/) is a purely functional programming language
|
2020-05-20 13:31:24 +03:00
|
|
|
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
|
|
|
|
2023-11-11 19:09:23 +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)
|
2023-11-11 19:09:23 +03:00
|
|
|
+ [Resources for learning Idris](https://github.com/idris-lang/Idris2/wiki/Resources),
|
2023-11-11 19:10:13 +03:00
|
|
|
including [videos](https://github.com/idris-lang/Idris2/wiki/Resources#official-talks)
|
|
|
|
that showcase its capabilities
|
2022-09-20 00:36:45 +03:00
|
|
|
+ [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
|
|
|
|
2023-11-11 19:02:33 +03:00
|
|
|
+ Cumulativity (currently `Type : Type`. Bear that in mind when you think
|
|
|
|
you've proved something)
|
2022-09-20 00:36:45 +03:00
|
|
|
+ `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-11 19:02:33 +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. This [map][3] should
|
|
|
|
help you find your way around the source code. See [the wiki page][4]
|
|
|
|
for more details.
|
2023-11-10 02:13:07 +03:00
|
|
|
|
|
|
|
[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>
|
2023-11-11 05:11:50 +03:00
|
|
|
[3]: <https://github.com/idris-lang/Idris2/wiki/Map-of-the-Source-Code>
|
2023-11-11 05:10:17 +03:00
|
|
|
[4]: <https://github.com/idris-lang/Idris2/wiki/Getting-Started-with-Compiler-Development>
|