Lean: Elaboration

• Elaboration: from syntax to Expr
  2026-10-01 · Ryan Williams
  LeanLean: Elaboration

  Part 2 of Lean from the Inside. What you type is much shorter than what the kernel checks. 1 + 1 leaves out the type, the addition instance and how the numerals are interpreted, and Lean fills all of that in before the kernel sees anything. That process is elaboration. This post follows a term from text to kernel term, then looks at the main things the elaborator fills in: metavariables and unification, implicit arguments, instances and coercions.