A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
⚗️ | Soma is a general-purpose dependently-typed functional programming language powered by Interaction Nets with a minimal runtime.
🧊 Модальна гомотопічна система
Program Specification in Lean 4
A sound and complete solver for type inhabitation and unification in dependent type theory, written in 185 lines of Lean.
Formally verified MBSE framework in Lean 4 — dependent type semantics for SysML v2 / KerML with V&V matrix completeness by type checking
A newbie's reference solutions to Lean tutorials
Exercises from Theorem Proving In Lean
Answers to the exercises in the Lean tutorial
Lean Toolchain provides a collection of formally verified cryptographic algorithms, mathematical operations, and data parsing utilities. All implementations are proven correct in Lean 4 and can be extracted to high-performance Rust code.
Working through Theorem Proving in Lean4
Working through Functional Programming in Lean
Add a description, image, and links to the dependent-types topic page so that developers can more easily learn about it.
To associate your repository with the dependent-types topic, visit your repo's landing page and select "manage topics."