appendix sectionnotation

Polymorphic record compilation

symbol	meaning	owner
symbol	meaning	owner
${{ℓ_{i} : τ_{i}}}_{i = 1}^{m}$	kind requiring the listed fields without fixing the complete record layout	definition 8.1
$idx (ℓ, τ)$	singleton target type inhabited by the canonical one-based position of $ℓ$ in $τ$	definition 8.8
$idx (ℓ, τ) \Rightarrow_{i} υ$	target type taking a certified layout index before returning $υ$	definition 8.11
${pos}_{ℓ} (τ)$	one-based position of $ℓ$ in a concrete record type sorted by label	definition 8.8
$C ⟨ J ⟩$	target vector selection, distinct from type application $C [τ]$	definition 8.11
$M ⇓_{R} v, C ⇓_{V} A$	source and target termination at values	lemma 8.12
$M ⇑_{R}, C ⇑_{V}$	source and target divergence	lemma 8.12
$ν_{S}$	numeral substitution sending $I_{t, ℓ}$ to ${pos}_{ℓ} (S (t))$	definition 8.9
$M ⇝_{rec} C$	derivation-directed compilation from an arbitrary source term to a target term	definition 8.14
$R_{rec}^{σ}$	closed source/target term relation at closed type $σ$	definition 8.18