A purely functional programming language with first class types

A dependently typed programming language, a successor to Idris

A prototype successor to Idris

Programming language agnostic type construction language based on polynomials.

formally verified category theory library

Language Server for Idris2

Sample code from "Type Driven Development with Idris"

Type-safe physical computations and unit conversions in Idris ⚖ 🌡 ⏲ 🔋 📐

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

A core language and API for dependently typed languages

TParsec - Total Parser Combinators in Idris

Type provider library for Idris

Utilities and documentation for exploring idirs2's new elaborator reflection.

Recursion schemes for Idris

GRIN backend for Idris

Experimental effects library for Idris 2

Idris Todo web application example

State machines in Idris

Idris Binary Integer Arithmetic, porting PArith, NArith, and ZArith from Coq

Transducers for Idris: a library for composable algorithmic transformation.

Command line interface library in Idris

Functional Pearl: Certified Binary Search in a Read-Only Array

Experiments with sequent calculi

An Idris type provider for communicating type-checkable protocols.

Idris, but it's C

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

Data frames for Idris 2

An extensible IO-like monad-like thing for Idris, with support for including linear subprograms