appendix sectionnotation

Frameworks, names, and contextual objects

symbol	meaning	first
symbol	meaning	first
$Γ ⊢_{Σ} M : A$	LF object typing under signature $Σ$	chapter 23
$Γ ⊢_{Σ} M can : A$	canonical, beta-normal eta-long LF object	definition 61.2
$⌜ - ⌝$	compositional representation into a framework	definition 61.5
$π \cdot x$	action of a finite atom permutation on $x$	definition 62.1
$supp (x)$	least finite support of a nominal element	definition 62.2
$a # x$	atom $a$ is fresh for $x$	definition 62.2
$[a] x$	nominal name abstraction	definition 62.4
$[Ψ ⊢ A]$	contextual type with ordinary-variable domain $Ψ$	definition 63.1
$u :: A [Ψ]$	modal declaration of an open object	definition 63.1
$clo (u, σ)$	closure of $u$ by contextual substitution $σ$	definition 63.1
$(M [N / x])_{A}^{n}$	hereditary substitution on normal objects, indexed by $A$	definition 63.5
$R / / x$	atomic component of a contextual simultaneous substitution	definition 63.5