A purely functional programming language with first class types
Go to file
Joel Berkeley ee18555869
Add (++) for List variation of All (#3179)
* Add `(++)` for `All` for `List`

* changelog

* contributors

* review changes

* update comment

* update comment

* match TODO style

* disambiguate the right one

* further comment changes
2024-01-01 21:03:13 -06:00
.github [ cleanup ] Post v0.7.0 cleanup 2023-12-25 13:49:26 +00:00
benchmark [ refactor ] Remove Data.Strings module (#1607) 2021-06-28 13:48:37 +01:00
bootstrap [ rc ] 0.7.0-rc2 2023-12-22 14:44:30 +01:00
docs [ rc ] Prepare for 0.7.0 2023-12-22 14:44:30 +01:00
icons Add icons 2020-05-20 18:48:55 +01:00
ipkg [ refactor ] S-Exp protocols to depend on fewer Idris modules (#3060) 2023-08-31 11:53:14 +01:00
libs Add (++) for List variation of All (#3179) 2024-01-01 21:03:13 -06:00
lint Lint utility 2021-01-16 10:00:03 +00:00
nix Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
Release [ admin ] Update checklist for v0.7.0-rc2 2023-12-22 14:44:30 +01:00
samples [ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00
src Add (++) for List variation of All (#3179) 2024-01-01 21:03:13 -06:00
support [ fix ] Correctly manage the empty file case while reading a file 2023-12-21 13:30:30 -06:00
tests [ test ] Add tests for GetOpt 2023-12-30 14:22:51 -06:00
www [ fix ] missing modules in .ipkg files (#3124) 2023-10-27 20:37:00 +01:00
.editorconfig [ install ] Check if 'realpath' exists for Chez and Racket backends (#1210) 2021-04-06 15:42:04 +01:00
.gitattributes Mark bootstrap code as generated 2021-06-30 22:11:54 +01:00
.gitignore [ test ] Set IDRIS2_PREFIX to a local dir when testing 2023-10-04 14:34:03 +01:00
.readthedocs.yaml [ docs ] fix build by adding config file 2023-11-23 17:46:45 +00:00
bootstrap-stage1-chez.sh Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
bootstrap-stage1-racket.sh Write files into bootstrap-build directory during bootstrap 2021-07-04 03:17:13 +01:00
bootstrap-stage2.sh Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
CHANGELOG.md Add (++) for List variation of All (#3179) 2024-01-01 21:03:13 -06:00
config.mk Fix build on FreeBSD (#2852) 2023-01-14 08:19:12 -06:00
CONTRIBUTING.md [ docs ] Update contributing guidelines 2023-07-18 17:27:20 +01:00
CONTRIBUTORS Add (++) for List variation of All (#3179) 2024-01-01 21:03:13 -06:00
default.nix [ ci ] Simplify bootstrap process in nix (#2731) 2022-10-28 19:29:30 +01:00
flake.lock Update flake 2023-01-07 17:32:48 -06:00
flake.nix Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
idris2.ipkg [ cleanup ] --timing levels 2022-04-13 14:37:43 +01:00
idris2api.ipkg [ cleanup ] Post v0.7.0 cleanup 2023-12-25 13:49:26 +00:00
INSTALL.md [ rc ] For v0.6.9 - to see if the process was right 2023-12-22 14:44:30 +01:00
LICENSE Add licence and changelog and update REAMDE 2020-05-20 11:31:48 +01:00
Makefile Separate support derivation (and small related tweaks to the Makefile) (#3172) 2023-12-27 08:14:03 -06:00
README.md wording 2023-11-13 11:42:27 +00:00

Idris 2

Documentation Status Build Status

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

Things still missing

  • Cumulativity (currently Type : Type. Bear that in mind when you think you've proved something)
  • rewrite doesn't yet work on dependent types

Contributions wanted

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.