Lean: Foundations

• Foundations: what an inductive type gives you
  2026-10-01 · Ryan Williams
  LeanLean: 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.