appendix sectionnotation

Graded extraction and partial computations

notation	meaning	owner
notation	meaning	owner
$γ ▸ t$	paper usage judgment in which the usage context $γ$ assigns one grade to each variable of the typing context for source term or type $t$	chapter 101
$Γ ⊩_{l} A$	level-indexed reducibility judgment imported from the pinned Agda development	theorem 101.7
$x ⇓ a$ , $x ⇑$	finite convergence and coinductive divergence of a partial computation	chapter 43
$x ⊑ y$ , $x ≫ = f$	approximation order and monadic bind on partial computations	chapter 43