| Volume | Chapter | Completed (excluding informal proof) |
|---|---|---|
| LF | Basics | ✅ |
| LF | Induction | ✅ |
| LF | Lists | ✅ |
| LF | Poly | ✅ |
| LF | Tactics | ✅ |
| LF | Logic | ✅ |
| LF | IndProp | weak_pumping; palindrome_converse; filter_challenge & filter_challenge_2... |
| LF | Maps | ✅ |
| LF | Imp | |
| LF | Auto | |
| LF | Rel | ✅ |
| LF | ProofObjects | |
| LF | IndPrinciples | |
| LF | ImpParser | |
| LF | ImpCEvalFun | |
| LF | Extraction |