appendix sectionnotation

Rewriting, shape, quantity, and graded modality

notation	meaning	owner
notation	meaning	owner
$ℓ ⟼ r$ , $t ⟶_{Σ} u$	declared signature rule and compatible signature reduction	chapter 39
$t ⟶_{β} u$ , $t ⟶_{β Σ} u$	framework beta step and combined beta/signature step	chapter 39
$t ⟶_{Σ b} u$ , $A \equiv_{β Σ} B$	signature rewriting modulo beta and generated conversion	chapter 39
$Sh (A)$ , $R \equiv_{ev} R^{'}$	parameter shape and common-value equality of parameter terms	chapter 40
$Γ_{1} + Γ_{2}$ , $k Γ$	pointwise context-use addition and scalar use	chapter 40
$Γ ⊢ S \equiv T$ , $Γ ⊢ M \equiv N :^{σ} S$	quantitative type and quantity-indexed term equality judgments	chapter 41
$Γ_{1} + ρ Γ_{2}$	substitution demand: ambient demand plus binder-scaled argument demand	chapter 41
$(Δ ∣ σ_{s} ∣ σ_{t}) ⊙ Γ ⊢ t : A$	triangular context, subject, and subject-type grade judgment	chapter 100
$Δ^{'} \ j$ , $Δ^{'} / j$ , $(Δ^{'} / j) * σ$	zero-based column discard, choice, and scaled insertion for graded substitution	chapter 100
$◻_{s} A$ , $t ⟶_{β} t^{'}$ , $(Δ ∣ σ_{s} ∣ σ_{t}) ⊙ Γ ⊧ t : A$	first-class graded modality, restricted GrTT beta step, and semantic typing validity	chapter 100