A purely functional programming language with first class types

A dependently typed programming language, a successor to Idris

Software Foundations in Idris

𝛌 Awesome Idris resources

formally verified category theory library

Parser combinators for Idris

Collection of Idris tests and demonstration programs

Koans are small lessons on the path to enlightenment. The aim of the Idris Koans project is to provide an easy learning environment in Idris. Your insight will be derived by encountering failing co…

Idris version of Domain Modeling Made Functional Book.

Type provider library for Idris

A test framework for Idris

Experiments in Idris / Unity integration.

Idris Todo web application example

State machines in Idris

A library for composable and effectful production, transformation and consumption of streams of data in Idris

Probabilistic computation in Idris

Transducers for Idris: a library for composable algorithmic transformation.

ITT: quantified dependent calculus with inference of all modalities, implemented in Idris 2

Homotopy Type Theory proofs in Idris

Ring solver for Idris

Velo is a tiny language (STLC + Hutton's Razor with Bools) to showcase & explore efficient verified implementations in Idris2.

Experiments in implementing functional data structures in Idris

Formalization of Tendermint proposer election properties

Dependently-typed structures for quantum physics in Idris

Experiments with dependent modal types