Lean - Interacting with Lean, Inductive Types & Recursion

This session we'll be reading from Theorem Proving in Lean 4 (TPiL) and focusing on chapters 6–8.
Reading (before the meetup)
- TPiL Ch 6: Interacting with Lean
- TPiL Ch 7: Inductive Types
- TPiL Ch 8: Induction and Recursion
In session
- Pattern matching, wildcards & overlapping patterns
- Structural recursion and induction
- Well-founded recursion and match expressions
Exercises — TPiL Ch 7 · Inductive Types (§7.10)
- Exercise 1–4
Exercises — TPiL Ch 8 · Induction and Recursion (§8.11)
- Exercise 1–5