Lean
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.
-
Lean from the Inside: why I'm writing this
The motivation, roadmap, and checked examples behind this learning log.
-
Foundations: what an inductive type gives you
Inductive types, universes, and the recursors behind functions and proofs.
-
Log: rfl proves equations, decide proves decidable propositions
A small experiment in the difference between definitional equality and decidable propositions.
-
Tactics: what a tactic proof builds
How tactic scripts build proof terms, manage goals, and power automation.