appendix sectionnotation

Modular type classes and implicit evidence

symbol	meaning	first
symbol	meaning	first
$K [τ]$	atomic class signature $K$ realized at carrier $τ$	chapter 16
$Θ ⊢ K [τ] ⇓_{res} V$	head-directed construction of module evidence	chapter 16
$\Rightarrow_{\mod}$	total module-functor interface arrow	chapter 16
$Γ; Θ ⊢ e : τ ⇝ e^{'}$	evidence-inserting term elaboration	chapter 16
$P ⪯ S$	coercive matching of a module path against a required signature	chapter 16
$Σ_{0} ⇓_{cn} (Σ; σ; δ)$	complete residual-constraint normalization	chapter 16
$Σ_{0} ⇝_{cn} (Σ; σ; δ)$	one residual-constraint reduction step	chapter 16
$I; Γ ⊢ S ⇓_{cand} {V_{1}, \dots, V_{n}}$	modular-implicit candidate set after type-component solving	chapter 16
$T_{1} ? \to T_{2}$	SI implicit function type	chapter 16
$\Rightarrow, \Rightarrow_{↓}, \Leftarrow$	algorithmic output, normalized output, and checking directions	chapter 16