Implementing Dependent Type Theory Inhabitation and Unification (opens in new tab)

arXiv:2603.01463v1 Announce Type: new Abstract: Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synthesis. We introduce Canonical-min, a sound and complete solver for inhabitation and unification in dependent type theory, implemented in 185 lines of Lean code. This paper describes a novel implementation of dependent type theory and a monadic framework to transform th...