Lean: Foundations
Part of Lean from the Inside. Follow the series in reading order or explore the entries below.
-
Foundations: what an inductive type gives you
Inductive types, universes, and the recursors behind functions and proofs.