blob: 20f0dcace22c5225535765e755270dcd9bacc886 [file] [view] [edit]
# Inductive Types
[Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.