Strict data rows

symbol	meaning	owner
symbol	meaning	owner
$\rho ,{ϵ}_{\rho },\{\ell :\tau \mid \rho \}$	row, empty row, and row extension; braces alone do not form a record type	definition 4.1
$\mathsf{Rec}(\rho ),\mathsf{Var}(\rho )$	record and variant types formed from the same row	definition 4.1
$\rho \mathrm{\backslash }\ell$	lacks predicate: row $\rho$ omits label $\ell$; not subtraction	definition 4.2
$p\Downarrow \mathrm{\top },\mathrm{\perp },p^{\prime }$	deterministic normalization of one lacks predicate	definition 4.2
$\mathsf{nf}(P)$	normalized finite predicate context, failing at $\mathrm{\perp }$	definition 4.2
$P⊩p$	symbolic entailment of a lacks predicate	definition 4.2
$G{\vDash }_{\mathsf{g}}P$	semantic satisfaction by a ground strict-row assignment	definition 4.6
$P⊢\rho \mathsf{row}$	strict unique-label row formation	definition 7.4
$a{\equiv }_P{a}^{\prime }$	formed row/type equality by permutation of distinct labels	definition 4.3
$S:P\to Q$	admissible sorted substitution between predicate contexts; not an object-language arrow	definition 7.3
$a[S],S;T$	postfix type/row/predicate substitution; first $S$, then $T$	definition 7.3, lemma 4.11
$P\Rightarrow \tau$	qualified type $\tau$ under lacks assumptions $P$	definition 4.6
$\mathrm{\Gamma }{⊢}_{q}e:P\Rightarrow \tau$	qualified source typing	definition 4.7
${\mathsf{insert}}_P(\ell :\tau ,\rho )$	constrained exposure of field $\ell$ with a residual row	definition 4.23
$\mathsf{solve}(P;E)=(U,Q)$	deterministic constrained type-and-row solve	definition 4.23
${\mathsf{W}}_r(\mathrm{\Gamma },e)=(P,S,\tau )$	qualified Algorithm W result	definition 4.29
$P{⊢}_{\mathsf{reg}}S:\mathrm{\Gamma }$	regularity/formation check for an inference substitution	definition 4.32
$\mathrm{\Delta }⊢d:\rho \mathrm{\backslash }\ell$	static lacks derivation elaborated as an offset expression	definition 4.36
$\mathsf{lay}(\tau ),\mathsf{lay}(\rho )$	named syntax translation to canonical target layouts	definition 4.39
$\mathsf{canTy}(\theta )$	recursively sorted canonical target type image used by T-Conv	definition 4.38, lemma 7.49
${\mathsf{ins}}_i(w,A)$	length-increasing insertion of $w$ at zero-based position $i$ in array $A$	definition 7.51
$\mathrm{ftv}(P)\subseteq \mathrm{ftv}(\mathrm{\Gamma },\tau )$	unambiguous open evidence interface	definition 7.53

Row-symbol boundary.

The rows in this section are strict, unique-label data rows with permutation equality and lacks predicates. They are not the duplicate-label effect rows of chapter 25: those use a different extension equation, exposure algorithm, inference theorem, and operational meaning.