The type system definition pays particular attention to the mode of the typing judgment, in the sense of logic programming (Debray and Warren 1988).
the type context and term are in­terpreted as inputs to the typing judgment, while the term's type is viewed as an output