appendix sectionnotation

Gradual types and casts

symbol	meaning	first
symbol	meaning	first
$?$	unknown gradual type	chapter 11
$A \sim_{c} B$	gradual consistency	chapter 11
$fun (A)$	partial function matching	chapter 11
$⟨ B \Leftarrow A ⟩^{p} a$	cast from $A$ to $B$ owned by $p$	chapter 11
$\bar{p}$	complementary blame face	chapter 11
$gnd (A)$	ground run-time tag of $A$	chapter 11
$Γ ⊢ e ⇝ a : A$	source-to-cast elaboration	chapter 11
$A ⊑_{ty} A^{'}$	type precision	chapter 11
$Γ ⊑_{ctx} Γ^{'}$	context precision	chapter 11
$e ⊑_{src} e^{'}$	source-term precision	chapter 11
$A ⪯^{\pm} B$	positive or negative blame-safety order	chapter 11
$Δ ⊢ a : A ⊑_{C} a^{'} : A^{'}$	typed target precision	chapter 11
$ρ ⊑_{e n v} ρ^{'}$	related closing substitutions	chapter 11
$F ⊑_{F} F^{'}$	related evaluation frames	chapter 11
$χ (T, S), cw (a), st (a)$	descriptor weight, total cast weight, and lexicographic stutter measure	chapter 11
$a ⟼^{ω}$	infinite target reduction	chapter 11
$S ⟺ T$	simple/dependent compatibility in the separate SD card	definition 23.53
${SD}_{S}^{T} (t), {DS}_{T}^{S} (s)$	dependent-to-simple and simple-to-dependent boundaries	definition 23.53
$t \tilde{=} t^{'} ▹ q$	dependent index guard in SD	definition 23.53