appendix sectionnotation

Dimensions and units of measure

symbol	meaning	owner
symbol	meaning	owner
$d =_{D} e$ , $d \neq_{D} e$	equality or inequality of normalized dimension maps over the fixed variable set $D$	chapter 6
$Num [d]$	rational numbers carrying dimension $d$	chapter 6
$q @ u$	rational literal expressed in compound unit $u$	definition 6.3
$fdv (a)$	free dimension variables, disjoint from ordinary type variables	definition 6.4
$A; D ⊢ τ type$	two-sorted formation of an ordinary/dimension type	definition 6.4
$munify (E)$	sorted type unifier with one Smith solve for the call’s dimension store	definition 6.16
$ρ_{E}$	principal dimension substitution returned for the ordered system $E$	definition 6.12
$I_{U} (Γ, e) = (S, τ)$	dimension-aware principal inference	definition 6.16
${elab}_{U} (D)$	derivation-directed elaboration to the monomorphic canonical-unit core	definition 6.22
$o \approx_{A} o^{'}$	related closed outcomes under a coherent unit change	definition 6.30