blob: f93a81fc00bcc815226c1e86d344f3199544a2f2 [file] [view] [edit]
# Inductive Types
[Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html) has a chapter about inductive datatypes.