Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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.