linear - Profunctor optics for linear types. States - State machines in Idris. Blodwen - Prototype implementation of Idris 2. Idris 2 - Pre-alpha implementation of Idris 2, the successor to Idris. Typedefs - Programming language-agnostic, algebraic data type definition language, written in Idris. Elba - Package manager for Idris. libc.idr - Bindings to the C standard library for Idris2. Inigo - Package manager for Idris 2 to help use and share Idris code. SPLV 2020 - Course notes and supporting code for the Scottish Programming Language and Verification summer school course on "The Implementation of Idris 2". idris2-elab-util - Utilities and documentation for exploring idirs2's new elaborator reflection. idris2-sop - Idris port of Haskell's sop-core and generic-sop libraries. Idrall - Dhall bindings for Idris. idris-ide-client - TypeScript library for communicating with an Idris IDE process. Frex - Programming with equations using free extensions. (Web) Katla - LaTeX code listing generator for Idris2. ITT in Idris - Quantified dependent calculus with inference of all modalities, implemented in Idris 2. Idris2GL - Graphics Library for Idris 2. idris2dart - Idris 2 code generator that outputs Dart code. DepSec - Static Information-Flow Control in Idris. TyRE - Dependently-typed regex parser in Idris 2. idris2-eff - Extensible, stack safe effects for Idris2. Katla - LaTeX & HTML code listing generator for Idris2. Collie - Command line interface for Idris2 applications. sirdi - Simple package manager for Idris 2. idris2-nvim - Simple configuration and extra tools for NVIM + LSP + Idris2.