2.1 How the traces are verified🔗ℹ

Every reduction step shown in the trace chapters lives as data in "traces/paths.rkt". Requiring that module — which happens on every build of this manual — re-verifies each step against the Redex model’s vc-eval relation (via must-step, up to α-equivalence) and checks that each final term is a genuine normal form. The same paths are covered in CI by

which additionally cross-checks every curated answer against run, the evaluator that explores the entire reduction graph. A failure means a reduction step no longer matches the model — the error message lists the actual successors, making it easy to identify which rule changed.