Canonical for Automated Theorem Proving in Lean

Chase Norman, Jeremy Avigad

Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to…