Lean: Elaboration
Part of Lean from the Inside. Follow the series in reading order or explore the entries below.
-
Elaboration: from syntax to Expr
Follow a term from surface syntax through unification and implicit arguments to a kernel expression.