Pinned Loading

1. Canonical Canonical Public

   Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

   Lean 89 7

2. CanonicalLean CanonicalLean Public

   A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

   Lean 111 10

3. Canonical-min Canonical-min Public

   A sound and complete solver for type inhabitation and unification in dependent type theory, written in 185 lines of Lean.

   Lean 8

4. AnkiChess AnkiChess Public

   Python

5. Composer Composer Public

   Composes 4 part chorales in the style of the common practice period.

   Java

6. Harmony Harmony Public

   Solving Harmony.

   Java