Lean - Type Classes & First Taste of Proofs

​Meetup 2 — Type Classes & First Taste of Proofs
This session introduces type classes — Lean's mechanism for overloading and abstraction, and the foundation for almost everything that follows, including functors and monads. We'll cover how to define instances, how Lean searches for them, and the standard classes you'll reach for constantly. In the second half we take a first look at one of Lean's defining features: propositions as types, the idea that a proof is simply a value whose type happens to be a statement. These first proofs are kept small and approachable, so you can build intuition before the proving sessions that follow.
Reading (before the meetup)
FPiL: Overloading and Type Classes + Interlude: Propositions, Proofs, and Indexing
TPiL: Dependent Type Theory; skim Interacting with Lean as reference.
In session
Type classes vs. interfaces, instance search, coercions, standard classes.
First encounter with Prop and propositions-as-types.
Exercises — FPiL Ch 3 · Overloading and Type Classes
- Ex 1 (§3.1 Positive Numbers), Ex 6 (§3.3 Controlling Instance Search), Ex 8 (§3.5 Standard Classes)
Exercises — FPiL Interlude · Propositions, Proofs, and Indexing
- Ex 1, 2, 3 (chapter Exercises — the Interlude is unnumbered)