appendix sectionnotation

Declaration processing

notation	meaning	owner
notation	meaning	owner
$I; ϵ; δ ⊢ A pos$	signed occurrence check for one mutual-family component, with ancestry state $δ$	chapter 122
$H_{\vec{P}} (A, x)$ , ${ih}_{\vec{P}} (A, x)$	hypothesis type generated from an accepted field type, and its constructor-computation term	chapter 122
${Empty}_{Timpl}$ , $B l o c k - c o m p$	Timpl’s encoded empty target and the simultaneous block’s constructor computation rule	chapter 122
$Θ; x ⊢ u desc x$ , $μ_{i}^{S}$ , ${DChild}_{S}$ , $R_{S}$	direct structural descent, the discipline-specific measure and child relation, and its tagged inverse image on a recursive component	chapter 123
$t ⇓_{R} v$ , $t ⇓_{RC} v$	closed evaluation for an accepted recursive source group and for its compiled accessibility-recursive target	chapter 123
$⊢ G guarded$ , $t ⇓_{T} n$ , $t ⇓_{T, cbv} v$	stream-group guardedness, extended-NbE subevaluation to the unique typed normal form, and its optional call-by-value implementation layer	chapter 124
$Θ ∣ M ⟹_{ct} Q$ , $e ⇓_{C} w$	dependent copattern clause-tree compilation and weak-head right-side evaluation	chapter 125
$‖ Q ‖$ , $q ⟹_{in} c$ , $c {⇓_{CC}}_{o} v$	translation of a typed dependent copattern tree to Tcop-core and deterministic outer-beta preparation followed by its distinct finite target-observation relation	chapter 125
$Γ ⊢ e runtime$ , $Γ ⊢ e erased$	relevance judgments selecting represented and deleted source phrases	chapter 126
$v R w$ , $Obs (q, o, w)$	source/target value representation and finite target-stream observation	chapter 126
$\| e \|$ , $(-)^{\circ}$	Timpl-to-Texec erasure and System Fi index erasure	chapter 126