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.
Progress is kept in this browser until you sign in
- An enumeration and a general cycle lawTraffic lights: define a transition and prove its cycle for every constructor.12 min
- Define your own typeDeclare constructors, match on all of them, and meet the missing-case error.11 min
- Prove two-sided inverse operationsShow next and previous cancel in both orders across every constructor.13 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
- Derive the fold for your own typeOne function parameter per constructor, read straight off the declaration.15 min