4.2 Typed terms
As objects of type theory, terms are subjected to type discipline. The well typing of a term depends on a set of declarations of variables we call a context. A context G is written [x1:T1;..; xn:Tn] where the xi's are distinct variables and the Ti's are terms. If G contains some x:T, we write (x:T)ÎG and also x ÎG. Contexts must be themselves well formed. The notation G::(y:T) denotes the context [x1:T1;..;xn:Tn;y:T]. The notation [] denotes the empty context.We define the inclusion of two contexts G and D (written as G Ì D) as the property, for all variable x and type T, if (x:T) Î G then (x:T)Î D. We write |D| for the length of the context D which is n if D is [x1:T1;..; xn:Tn].
A variable x is said to be free in G if G contains a declaration y:T such that x is free in T.
Environment.
Because we are manipulating constants, we also need to consider an environment E. We shall give afterwards the rules for introducing new objects in the environment. For the typing relation of terms, it is enough to introduce two notions. One which says if a name is defined in the environment we shall write c Î E and the other one which gives the type of this constant in E. We shall write (c : T) Î E.In the following, we assume E is a valid environment. We define simultaneously two judgments. The first one E[G] |- t : T means the term t is well-typed and has type T in the environment E and context G. The second judgment WF(E)[G] means that the environment E is well-formed and the context G is a valid context in this environment. It also means a third property which makes sure that any constant in E was defined in an environment which is included in G (This requirement could be relaxed if we instead introduced an explicit mechanism for instantiating constants. At the external level, the Coq engine works accordingly to this view that all the definitions in the environment were built in a sub-context of the current context.).
A term t is well typed in an environment E iff there exists a context G and a term T such that the judgment E[G] |- t : T can be derived from the following rules.
- W-E
WF ([])[[]] - W-s
WF (E)[G::(x:T)] - Ax
E[G] |- Prop : Type (p) E[G] |- Set : Type (q)
E[G] |- Type (i) : Type (j) - Var
E[G] |- x : T - Const
E[G] |- c : T - Prod
E[G] |- (x:T)U : s2
E[G] |- (x:T)U : Type (k) - Lam
E[G] |- [x:T]t : (x:T)U - App
E[G] |- (t u) : T{x/u}