v1.4.19 — Fix confusing Nat-overload in two Ch. 1 §3 Vec examples
Reader-caught: “#eval (Vec.replicate 7 3 : Vec Nat 3)” used Nat for both
the vector’s element type and its length, making it hard to tell which
Nat played which role. Switched to Vec Int 3, storing -42 — visibly
numeric, but unmistakably not a length (negative, and no small Nat could
be it). Real/complex numbers were considered but ruled out: both are
Mathlib-only and noncomputable in Lean, so #eval cannot run them at
all, let alone this early in a book that stays Mathlib-free through
Chapter 11.
The dot-product example had the same problem one step further: renaming
v3/v2 to vecA/vecB only removed the naming coincidence, not the
underlying Vec Nat/Nat overlap. Switched Vec.dot itself to
Vec Int n → Vec Int n → Int, and both vecA/vecB’s and the Python
dot() example’s values to non-sequential numbers (17, -3, 42, 99, 8)
so no element value could be mistaken for a length either, keeping the
Python/Lean examples’ values in sync as before.
v1.4.19 — Fix a stale “Download PDF” badge in the root README
The root README’s “Download PDF” badge linked directly to the v1.4.14
release asset by exact filename, going stale as soon as v1.4.15
shipped (three releases behind by the time this was caught). Switched
to the version-less .../releases/latest/download/... alias, matching
the “Read the book” link above it, so it cannot go stale again.
v1.4.19 — Fix a Π-type family/type conflation and a forward reference
Reader-caught: “The general pattern: Π-types” (Ch. 1 §3) used B(x)
from its very first display formula without ever stating that B
itself has type A → Sort u (a family of types, not a type) — despite
later parts of the same section stating this explicitly. Added the
same statement at first use.
Also reader-caught, in the same section: “this is exactly what ∀ has
meant since Chapter 3” presupposed the reader had already read Chapter
3, which comes after Chapter 1. Reworded prospectively.
v1.4.19 — Fix a LaTeX build error: literal $ next to \mathbb
Two inline math spans of the form “$X = $” (a space immediately before
the closing $) violated Pandoc’s math-span rule (no whitespace
immediately inside $...$), leaking a raw \mathbb/similar command
out of math mode and crashing the LaTeX build. Found via a full-book
scan for the same pattern; fixed both instances (Ch. 1 §1, Ch. 6 §4).
Caught while rebuilding the PDF for this release.