appendix sectionnotation

Linear and affine types

symbol	meaning	first
symbol	meaning	first
$Γ; Δ ⊢ e : A$	reusable finite-map $Γ$ , exactly-once finite-map $Δ$ ; semicolon separates regimes	chapter 18
$Δ_{1} # Δ_{2}$	linear contexts with disjoint domains	chapter 18
$Δ_{1} ⊎ Δ_{2}$	disjoint union of linear contexts	chapter 18
$A \otimes B$	multiplicative tensor type	chapter 18
$A ⊸ B$	linear function type	chapter 18
$A \oplus B$	additive sum with shared branch residual	chapter 18
$! A$	duplicable value formed without linear resources	chapter 18
$Tok, H$	infinite token supply and finite live set	chapter 18
$H ⊩ e : A$	well-owned file-token configuration	chapter 18
$(H, e) ⟶ (H^{'}, e^{'})$	one file-token configuration transition	chapter 18
$(H, e) ⟶^{*} (H^{'}, e^{'})$	finite file-token configuration reduction	chapter 18
$H ⊩_{ρ} e : A$	file-token template typed in structural regime $ρ \in {ℓ, a, r, u}$	chapter 18
${use}_{z} (e)$	pathwise free-use count, when defined	chapter 18
$⊢_{ℓ}, ⊢_{a}, ⊢_{r}, ⊢_{u}$	linear, affine, relevant, and unrestricted regimes	chapter 18
$Q, 0, +, \cdot$	source-bounded rig of quantities for McBride’s dependent card	definition 36.32
$Ξ ⊢_{q} T ∋ t$ , $Ξ ⊢_{q} e \in S$	quantity-indexed checking and synthesis over one marked precontext	definition 36.32
$(p x : S) \to T$	dependent function with unit price $p$	definition 36.32