Inductive types and case analysis
Enumerations, constructors with data, and trees. You will define inductive types, write functions over them by pattern matching, and prove properties by exhaustive case analysis and structural induction.
Sign in to track your progress
- An enumeration and a function on itTraffic lights: a type with three values and a next function.10 min
- Cover every constructorcases l <;> rfl proves a cycle for all three lights.10 min
- Constructors that carry dataShapes with sizes, and a scaling law proven per constructor.12 min
- Binary treesEvery tree has positive size.11 min
- Induction over treesTwo induction hypotheses, one for each subtree.14 min