← Changelog index

---

v1.4.20 — Fix a leaked blockquote marker, and add two worked examples

Reader-caught a rendering bug in the PDF: a > character was appearing repeatedly inside Chapter 1 §4’s “Programmer’s corner (Python)” box discussing β-reduction. Root cause: that one box, alone in the whole book, was written as a markdown blockquote (> prefix on every line) instead of the plain-paragraph format every other “Programmer’s corner”/”Mathematical reading” box uses — build_latex.py’s box-wrapping regex re-emits the captured body as a fresh paragraph, so the embedded > markers are no longer recognized as blockquote continuation syntax and leak through as literal > characters. Fixed the one affected box, and hardened wrap_reading_boxes() to strip any such markers defensively so a stray blockquote-formatted box can’t reintroduce this.

Also fixed a print-unsuitable reference (“The README states…”) in the same chapter, and added two worked, toolchain-verified examples:

• The Motive glossary entry only described “motive is not type correct” abstractly; added a genuine failing example (using Vec and a dependent pair) plus its subst-based fix, both tested directly against lean_project’s pinned toolchain.
• The Universal property entry named “products, quotients, and free constructions” but only worked through the product example; added a second worked example (the free-commutative-monoid-on-one-generator fact from Chapter 1 §1), with its own diagram.