So I will just contain myself in saying that we have contexts, which are sequences of variables with types, environments and two judgements, the first is that g is a word defined context and the other one is the term M as a given type.
| Now, it would
be interesting to go through briefly in some of the features of the calculus
of inductive constructions, which is essentially the specific constructive
type theory that here is taken as a metamodel. Of course we have time limits,
So I will just contain myself in saying that we have contexts, which are sequences of variables with types, environments and two judgements, the first is that g is a word defined context and the other one is the term M as a given type. |
|
