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
- Defining and extending structures
- Fields, constructors, and pattern matching on structures
- Type classes: definition and instances
- Deriving type class instances
- Practical examples of type classes in Lean 4

These chapters don't have built-in exercises — we encourage you to create your own exercises from the material and bring them to the session for discussion.