| ← Ch. 12: Working Efficiently | Table of contents | Appendix: Solutions → |
Learning objectives. By the end of this chapter, describe what this
book built entirely from scratch, translate that construction into
Mathlib’s class-based idiom and see two genuinely new facts it delivers
for free, and pick a next project — from the five scaffolded here, or the
Church-encodings aside — that extends material already in hand.
Sections
| ← Ch. 12: Working Efficiently | Table of contents | Appendix: Solutions → |