Lean — Ryan Williams

2026-10-01 · Ryan Williams

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.

Lean from the Inside: why I'm writing this

2026-10-01 · Ryan Williams

Lean

I use Lean for proofs about program analyses, but I learned it by imitation: copy a proof that works, change it until it works for my problem. This series is where I slow down and learn what is actually happening, from the type theory up through the elaborator, the tactics and the kernel.

The posts are notes for my future self first. If they help someone else, good.

Foundations: what an inductive type gives you

2026-10-01 · Ryan Williams

Lean Lean: Foundations

Part 1 of Lean from the Inside. Almost everything in Lean, from Nat to And to Eq, is an inductive type, and almost every function and proof about those types ends up as a call to a single function the kernel generates: the recursor. This post works out what that means. It covers what inductive adds to the environment, how universes and Prop constrain the recursor, and how a match you write becomes a recursor call.

Log: rfl proves equations, decide proves decidable propositions

2026-10-01 · Ryan Williams

Lean Lean: Log

Both of these close 2 + 2 = 4:

example : 2 + 2 = 4 := rfl
example : 2 + 2 = 4 := by⊢ 2 + 2 = 4 decideAll goals completed! 🐙

So I assumed they were interchangeable for small closed facts. They are not. rfl fails on 10 < 20:

example : 10 < 20 := Type mismatch
  rfl
has type
  ?m.9 = ?m.9
but is expected to have type
  10 < 20rfl

Tactics: what a tactic proof builds

2026-10-01 · Ryan Williams

Lean Lean: Tactics

Part 3 of Lean from the Inside. A tactic proof looks like a list of instructions, which makes it feel like a different thing from a term. It isn't. The kernel only checks terms, and a by block is a program that builds one. This post looks at what that program builds, how it keeps track of the goals it has left, what the main automation tactics produce, and how to write a tactic of your own.