A.2.1 Contexts
A context is a list
which indicates that the distinct variables are assumed to have types , respectively. The list may be empty. We abbreviate contexts with the letters and , and we may juxtapose them to form larger contexts.
The judgment formally expresses the fact that is a well-formed context, and is governed by the rules of inference
{mathpar}
\inferrule*[right=-emp]
\inferrule*[right=-ext]
x_1 : A_1, …, x_n-1 : A_n-1 ⊢A_n : _i
(x_1 : A_1, …, x_n : A_n)
with a side condition for the second rule: the variable must be distinct from the variables .
Note that the hypothesis
and conclusion
of -ext are judgments of different forms: the hypothesis says that in the context of variables , the expression has type ; while the conclusion says that the extended context is well-formed.
(It is a meta-theoretic property of the system that if is derivable
, then the context must be well-formed; thus -ext does not need to hypothesize well-formedness of the context to the left of .)
Title | A.2.1 Contexts |
---|---|
\metatable |