Typing contexts

typing context If $T_1, \ldots, T_n$ are type expressions and $x_i,\: i=1, \ldots, n$ are distinct individual variables, then x_i:T_i is a type assumptiontype assumption and the list $\hbox{$x_1\!:\!T_1, \ldots,$ } x_n\!:\!T_n$ is a typing contexttyping context. We let ${\cal T}, {\cal T}', {\cal T}_j$ denote typing contexts.