Typing judgment
= Typing judgment
{title2=$\Gamma\vdash e:\tau$}
A <typing judgment> asserts that expression $e$ has type $\tau$ under a <typing context> $\Gamma$. A rule displays prerequisite <typing judgments> above a line and their conclusion below it. Repeatedly applying rules gives a derivation; the addition example under <type system> uses two assumptions and one addition rule.