Inductive Types

Theorem Proving in Lean has a chapter about inductive datatypes.