1
2
Fork
You've already forked Idris2
0
A purely functional programming language with first class types https://github.com/idris-lang/Idris2
  • Idris 95.2%
  • C 2.5%
  • Scheme 0.6%
  • Racket 0.4%
  • Makefile 0.3%
  • Other 1%
Julio 0fb7253b8c
 [ fix ] parseDouble dropping - sign when whole = 0 ( #3805 ) 
* [ fix ] parseDouble dropping - sign when whole = 0
* changes from code review
* I contributed!
2026年07月09日 16:21:43 +01:00
.github [ fix ] update chez version in windows ci ( #3799 ) 2026年06月22日 11:06:37 +01:00
benchmark [ refactor ] Remove Data.Strings module ( #1607 ) 2021年06月28日 13:48:37 +01:00
bootstrap Revert bootstrap 2026年04月15日 14:11:40 +01:00
docs Bump idna from 3.11 to 3.15 in /docs 2026年05月27日 15:28:38 +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 [ fix ] parseDouble dropping - sign when whole = 0 ( #3805 ) 2026年07月09日 16:21:43 +01:00
lint Lint utility 2021年01月16日 10:00:03 +00:00
nix buildIdris cleanup ( #3793 ) 2026年06月20日 00:35:51 -05:00
Release [ test ] Clean version in tests output ( #3660 ) 2025年11月07日 15:25:01 +00:00
samples [fix] include stdio header in readline C code in example so it builds on all systems ( #3378 ) 2024年09月01日 08:57:24 -05:00
src [Zurihack] Small Driver refactor ( #3795 ) 2026年06月13日 00:27:09 +01:00
support fmt 2026年04月07日 02:20:12 +01:00
tests [ fix ] parseDouble dropping - sign when whole = 0 ( #3805 ) 2026年07月09日 16:21:43 +01: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 line length 2026年04月06日 18:12:04 +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 [ rc-admin ] Move changelog entries over 2025年10月31日 17:11:29 +00:00
CHANGELOG_NEXT.md [ fix ] parseDouble dropping - sign when whole = 0 ( #3805 ) 2026年07月09日 16:21:43 +01:00
CITATION.cff [ feature ] Add CITATION.cff 2025年08月24日 11:13:09 +01:00
config.mk [ fix ] Use HOMEBREW_PREFIX instead of /opt/homebrew 2024年04月27日 14:51:25 -07:00
CONTRIBUTING.md Reject by default non-human contributions ( #3755 ) 2026年04月04日 11:22:36 +01:00
CONTRIBUTORS [ fix ] parseDouble dropping - sign when whole = 0 ( #3805 ) 2026年07月09日 16:21:43 +01:00
default.nix [ ci ] Simplify bootstrap process in nix ( #2731 ) 2022年10月28日 19:29:30 +01:00
flake.lock flake lockfile was not regenerated after the source for idris2-mode was updated 2025年12月17日 09:45:22 +00:00
flake.nix [ nix ] Point emacs-src to idris-community/idris2-mode ( #3682 ) 2025年11月19日 08:06:00 -06:00
idris2.ipkg [ cleanup ] --timing levels 2022年04月13日 14:37:43 +01:00
idris2api.ipkg [ cleanup ] Simplify equality functions 2025年12月14日 10:56:03 +03:00
INSTALL.md [ rc-admin ] Bump version in INSTALL docs 2025年10月31日 17:11:29 +00:00
LICENSE Add licence and changelog and update REAMDE 2020年05月20日 11:31:48 +01:00
Makefile [ make ] Pass IDRIS2_PREFIX in install-libs 2025年11月05日 18:20:02 +03:00
README.md Update README with resources to learn and use Idris ( #3606 ) 2025年08月13日 00:01:13 +01: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

Installation and Packages

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.

Resources to Learn Idris 2

Books

Tutorials

Official talks

Community talks

Documentation

Docker images

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.