Lean - Induction & Recursion

​This session we'll be reading from Theorem Proving in Lean 4 (TPiL) and focusing on chapter 8.
Reading (before the meetup)
- TPiL Ch 8: Induction and Recursion
https://leanprover.github.io/theorem_proving_in_lean4/Induction-and-Recursion/#induction-and-recursion
In session
- Well-founded recursion and match expressions
- Structural recursion and induction (continued from last time)
- Pattern matching edge cases: overlapping patterns, wildcards
Exercises — TPiL Ch 8 · Induction and Recursion (§8.11)
- Exercise 1–5