Lean — Structures, Records & Type Classes

​This session we'll be reading from Theorem Proving in Lean 4 (TPiL) and focusing on chapters 9 and 10.

Reading (before the meetup)
- TPiL Ch 9: Structures and Records
https://leanprover.github.io/theorem_proving_in_lean4/Structures-and-Records/#structures-and-records
- TPiL Ch 10: Type Classes
https://leanprover.github.io/theorem_proving_in_lean4/Type-Classes/#type-classes

In session
- Structures and records in Lean 4
- Type classes: typeclass resolution, instances, and derivation
- Practical applications and patterns

Since these chapters do not have official exercises, we encourage readers to create their own exercises for discussion. Bring your questions and examples!