docs: publish normative Quon language reference (#378)

website/astro.config.mjs

@@ -55,7 +55,6 @@ export default defineConfig({
 						{ label: 'Putting it together', slug: 'language/putting-together' },
 					],
 				},
-<<<<<<< HEAD
 				{
 					label: 'Cookbook',
 					items: [
@@ -104,6 +103,7 @@ export default defineConfig({
 					label: 'Reference',
 					items: [
 						{ label: 'Feature support matrix', slug: 'reference/support-matrix' },
+						{ label: 'Language reference', slug: 'reference/language' },
 						{ label: 'quonc CLI', slug: 'reference/quonc' },
 						{ label: 'Compiler pipeline', slug: 'reference/compiler' },
 						{ label: 'Diagnostic catalog', slug: 'reference/diagnostics' },
@@ -116,40 +116,6 @@ export default defineConfig({
 						{ label: 'Style guide', slug: 'contribute/style-guide' },
 					],
 				},
-=======
-			{
-				label: 'Cookbook',
-				items: [
-					{ autogenerate: { directory: 'cookbook' } },
-				],
-			},
-			{
-				label: 'Reference',
-				items: [
-					{ label: 'quonc CLI', slug: 'reference/quonc' },
-					{ label: 'Compiler pipeline', slug: 'reference/compiler' },
-				],
-			},
-			{
-				label: 'Architecture',
-				items: [
-					{ label: 'Compiler internals', slug: 'architecture/compiler-internals' },
-					{ label: 'Neutral-atom model', slug: 'architecture/na-model' },
-				],
-			},
-			{
-				label: 'Guides',
-				items: [
-					{ label: 'Developer tooling', slug: 'guides/tooling' },
-					{ label: 'Backends and verification', slug: 'guides/backends' },
-					{ label: 'Results and plotting', slug: 'guides/results-and-plotting' },
-					{ label: 'Neutral-atom FT demo', slug: 'guides/na-ft-demo' },
-					{ label: 'Maturation path', slug: 'guides/roadmap' },
-					{ label: 'Application demos', slug: 'guides/applications' },
-					{ label: 'Creative & games', slug: 'guides/creative' },
-				],
-			},
->>>>>>> b09b4cb (docs: clarify Language, Reference, and Architecture handoffs (#386))
 			],
 		}),
 	],

website/src/content/docs/cookbook/bell.mdx

@@ -12,6 +12,8 @@ sidebar:
   Audit: website/scripts/audit-bell-walkthrough.sh
 -->
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#circuits).
+
 ## What we're building and why
 
 A Bell state is the simplest entangled quantum state: two qubits whose

website/src/content/docs/cookbook/bernstein-vazirani.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 4
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#circuits).
+
 ## What we're building and why
 
 The Bernstein–Vazirani algorithm solves a problem that would take n queries

website/src/content/docs/cookbook/grover.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 5
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#built-ins).
+
 ## What we're building and why
 
 Grover's algorithm is the quantum procedure that finds a marked item in an

website/src/content/docs/cookbook/index.mdx

@@ -197,7 +197,7 @@ each page focuses on:
 
 The examples assume familiarity with [circuits, linear quantum values, and
 `run` blocks](/language/). For the formal language definition, see the
-[Quon specification](https://github.com/arniber21/quon/blob/main/SPEC.md).
+[Quon specification](https://github.com/arniber21/quon/blob/main/SPEC.md). For the browsable normative reference — syntax, typing contracts, constraints, and minimal examples for every construct — see the [Language reference](/reference/language/).
 The cookbook pages reference specific files in the compiler's test suite —
 follow the links to read the raw `.qn` sources and their Python verifiers.
 

website/src/content/docs/cookbook/ising.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 7
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#gates).
+
 ## What we're building and why
 
 The transverse-field Ising model is the simplest non-trivial many-body

website/src/content/docs/cookbook/na-qaoa.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 10
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#circuits).
+
 ## What we're building and why
 
 The neutral-atom (NA) backend is Quon's flagship compilation target for

website/src/content/docs/cookbook/phase-estimation.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 14
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#gates).
+
 ## What we're building and why
 
 Quantum phase estimation (QPE) estimates the phase φ in the eigenvalue

website/src/content/docs/cookbook/qaoa.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 8
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#circuits).
+
 ## What we're building and why
 
 The Quantum Approximate Optimization Algorithm (QAOA) is a variational quantum

website/src/content/docs/cookbook/qft.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 6
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#expressions-and-statements).
+
 ## What we're building and why
 
 The Quantum Fourier Transform (QFT) is the quantum analogue of the discrete

website/src/content/docs/cookbook/samples.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 11
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language).
+
 import catalog from '../../../../../samples/catalog.yaml?raw';
 
 > **Optional detour.** This page is not part of the cookbook curriculum —

website/src/content/docs/cookbook/shor-kernel.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 9
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#circuits).
+
 ## What we're building and why
 
 Shor's algorithm is the quantum algorithm that factors integers in polynomial

website/src/content/docs/cookbook/teleportation.mdx

@@ -5,6 +5,8 @@ sidebar:
   order: 3
 ---
 
+> **Reference:** the Quon constructs in this recipe are defined normatively — syntax, typing contract, constraints, and a minimal example — in the [Language reference](/reference/language/#quantum-effects).
+
 ## What we're building and why
 
 Quantum teleportation is the protocol that transfers an unknown quantum state

website/src/content/docs/language/borrow.md

@@ -257,6 +257,8 @@ enforces that the qubit is consumed (no leak, no escape), but the *form* of
 consumption is now a programmer choice, not a language mandate.
 
 When a borrow block is rejected, the [diagnostic catalog](/reference/diagnostics/#monad-and-borrow) explains the escape or unconsumed-ancilla error and the supported repair.
+For the normative form of borrow blocks and ancilla cleanup — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#quantum-effects).
+
 ## Next
 
 For fault-tolerant computing, Quon introduces encoded logical qubits with

website/src/content/docs/language/circuits.md

@@ -323,6 +323,8 @@ The dynamic, effectful side (which you will meet soon) gets none of those
 optimizations, which is exactly why Quon keeps the two worlds separate.
 
 When a circuit composition fails, the [diagnostic catalog](/reference/diagnostics/) lists the exact error, a minimal reproducer, and the smallest repair.
+For the normative form of circuits and gate placement — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#circuits).
+
 ## Next
 
 Circuits act on qubits, but so far we have only referred to qubits by position.

website/src/content/docs/language/clifford.md

@@ -255,6 +255,8 @@ fixpoint iterates until no pass makes a change, so reductions that *enable*
 further peephole cancellations are caught in later rounds.
 
 When a Clifford annotation is rejected, the [diagnostic catalog](/reference/diagnostics/#refinement-clifford-and-depth) explains the mismatch and offers a repair.
+For the normative form of Clifford classification — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#clifford-classification).
+
 ## Next
 
 Now we leave the pure unitary world. The Quantum Monad allows allocation,

website/src/content/docs/language/depth.md

@@ -247,6 +247,8 @@ the typechecker's gift to the optimizer: a proven ceiling that makes
 aggressive rewriting safe.
 
 When a depth annotation is rejected, the [diagnostic catalog](/reference/diagnostics/#refinement-clifford-and-depth) explains the mismatch and offers a repair.
+For the normative form of depth bounds — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#depth-bounds).
+
 ## Next
 
 The fourth type parameter — Clifford classification — tells the compiler

website/src/content/docs/language/introduction.md

@@ -283,6 +283,7 @@ pages in order the first time; afterward each page stands on its own as a
 reference, and every page ends with a link to the next.
 
 When the compiler rejects your program, the [diagnostic catalog](/reference/diagnostics/) lists every error by family, with a minimal reproducer and the smallest supported repair.
+For the normative form of the language constructs above — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language).
 
 ## Next
 

website/src/content/docs/language/linearity.md

@@ -326,6 +326,8 @@ rules would all be checking properties of a program that might not even be
 physically realizable.
 
 For the exact diagnostic message and repair for each linearity error, see the [diagnostic catalog](/reference/diagnostics/#linearity).
+For the normative form of the linear type discipline — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#linearity).
+
 ## Next
 
 Now that you understand how resources are tracked, the next page shows how

website/src/content/docs/language/measurement.md

@@ -250,6 +250,8 @@ dynamic circuits. The pass preserves the observable result (the deferred
 CNOT is equivalent to the feed-forward correction) while changing the
 execution model.
 
+For the normative form of measurement and classical control — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#quantum-effects).
+
 ## Next
 
 Not all qubits need to be allocated up front. Borrow blocks let you

website/src/content/docs/language/monad.md

@@ -245,6 +245,8 @@ well-defined "before" and "after" state of the linear context, and the
 typechecker checks the transition at every `<-`.
 
 When a `<-` bind or `run` block is rejected, the [diagnostic catalog](/reference/diagnostics/#monad-and-borrow) explains the error and offers a repair.
+For the normative form of the Quantum Monad — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#quantum-effects).
+
 ## Next
 
 The most important effectful operation is measurement — and what you can do

website/src/content/docs/language/parallel.md

@@ -246,6 +246,8 @@ then emits `quantum.circ` ops directly from this tree — one MLIR gate op per
 input is the elaborator's output, and neither needs to know about the symbolic
 world the typechecker reasoned over.
 
+For the normative form of parallel and parametric composition — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#circuits).
+
 ## Next
 
 The depth bounds in these types are symbolic expressions with their own

website/src/content/docs/language/putting-together.md

@@ -290,6 +290,8 @@ This program exercised:
 - **The optimizer fixpoint** (five passes, convergence, no-op for this circuit)
 - **OpenQASM emission** (the final artifact)
 
+For the normative form of every construct in this program — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#implementation-status).
+
 ## Where to go next
 
 - **[Cookbook](../cookbook/)** — deeper worked examples: teleportation,

website/src/content/docs/language/qec.md

@@ -254,6 +254,8 @@ measurement — as a breakdown, which is essential for tuning the code distance
 against the hardware's coherence time.
 
 When a QEC type is rejected, the [diagnostic catalog](/reference/diagnostics/#qec-and-target-capability) explains the distance, family, or logical-operation error and the supported repair.
+For the normative form of QEC builtins — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#built-ins).
+
 ## Next
 
 Now you've seen every concept in the language. The final page walks through

website/src/content/docs/language/qubits.md

@@ -243,6 +243,8 @@ destructures it in the same binding. The typechecker verifies that the circuit's
 output width (2) matches the pattern's arity (2) — a width mismatch here is the
 same kind of error as the `qreg` mismatch above.
 
+For the normative form of qubit and register types — syntax, typing contract, constraints, and a minimal valid example — see the [Language reference](/reference/language/#types-and-kinds).
+
 ## Next
 
 You have now seen that qubits are linear values consumed exactly once — but we