How the books fit together
Argon’s documentation is three texts.
- The Argon Book — the language in order: the model, its types, its reasoning, incompleteness, composition, and execution.
- The Argon Reference — the exact rules. Terse, complete, canonical for the surface, and anchored to the Lean mechanization, which is canonical for the substrate. Where the Lean and the Reference disagree on something the Lean covers, the Lean wins; where this book and the Reference disagree on a rule, the Reference is correct.
- Argon by Example — runnable programs, compiled and run in CI. A broken example is a failed build, not a stale snippet.
RFDs record design decisions; the Lean mechanization carries the proofs.