Lean from the Inside

A learning log about how Lean 4 works: its type theory, the elaborator, tactics, the kernel, and metaprogramming. I'm writing it to learn Lean properly and to have notes I can come back to. Every code block on these pages is checked by Lean when the site builds, so the examples compile on the toolchain named in each post. Hover over code to see the types and proof states Lean inferred.

The series has two kinds of posts:

Log entries are short notes on one thing I learned, such as why rfl failed where decide worked.
Deep dives follow the roadmap below, from the surface of the language down to the kernel.

Roadmap

Foundations: dependent types, universes, Prop vs Type, inductive types and the recursors Lean generates for them.
Elaboration: how surface syntax becomes a kernel Expr, including metavariables, unification, implicit arguments, instances and coercions.
Tactics: what a tactic proof builds, how simp, omega and decide work, and writing a tactic in TacticM.
Kernel and trust (not yet written): what the kernel checks, the standard axioms, and what native_decide, partial and implemented_by add to the trusted base.
Programming (not yet written): structural and well-founded recursion, termination proofs, do notation, and the compiler.
Metaprogramming (not yet written): macros, syntax extensions, custom elaborators and small embedded languages.

Every post in the series is in the lean category. Each written part has its own category too: foundations, elaboration and tactics. Log entries are under lean-log.