appendix sectionnotation

Qualified types, evidence, and ML modules

symbol	meaning	first
symbol	meaning	first
$K τ$	unary class predicate at monotype $τ$	section 13.1
$P \Rightarrow τ$	qualified type under finite predicate set $P$	section 13.1
$C; P; Γ ⊢ e : τ$	canonical qualified source typing	section 13.2
${resolve}_{C, Δ} (p) = d$	deterministic dictionary-evidence construction	lemma 11.1
$C; P ⊩ Q$	class-evidence entailment from canonical assumptions	section 13.1
${nf}_{C} (P)$	substitution-natural canonicalization result $ok (Q, η)$ or $reject (p)$ , with factorizing evidence	lemma 11.2
$W_{C} (Γ, e)$	qualified Algorithm W result	section 13.2
$S ⋆ Γ$	canonical action of type substitution $S$ on a qualified typing environment, with evidence transport	section 13.2
$Δ_{Q} \Rightarrow_{e} Δ_{P}$	dictionary-evidence transport from the canonical telescope $Δ_{Q}$ to the required interface $Δ_{P}$	section 13.2
$⟨ ⟨ A ⟩ ⟩_{s}$	atomic module signature embedding the kind or type $A$	convention 16.13
$S^{†} u$	action of type substitution $S$ on evidence-core syntax or an evidence template	theorem 11.6
$⊢_{D}^{W} e : τ ⇝ u$	inference-indexed dictionary elaboration	theorem 11.6
$Ty$	kind of static constructors in the reduced module calculus	section 12.1
$B (u :: κ; τ)$	basic module signature	definition 12.1
$Sigma (X : σ_{1}) . σ_{2}$	dependent hierarchy signature	definition 12.1
$Pi (X : σ_{1}) . σ_{2}$	functor signature	definition 12.1
$Sing (c)$	singleton kind recognizing constructor $c$	section 12.1
$M . s, M . d$	static and dynamic projections of a basic module	definition 12.2
$κ_{1} ⪯_{k} κ_{2}$	module-calculus subkinding	section 12.2
$τ_{1} <: τ_{2}$	ordinary dynamic-type subtyping	section 12.2
$σ_{1} ⪯_{s} σ_{2}$	subsignature matching	section 12.2
$Pack (σ)$	target package/product/function type	definition 12.5
${mcoe}_{D}$	target coercion induced by matching derivation $D$	definition 12.6
${Open}_{σ} (z, X; q)$	scoped package opening	definition 12.5
$T_{ρ \to D} (M)$	derivation-indexed module-to-package translation	theorem 12.7
$psig (p)$	principal signature of a closed projectible path	definition 12.12