This section gives an overview of all relevant classes for extending MMT by additional type checking rules. The class relevant for checking judgments is checking.Solver. MMT uses the following judgments:
| Judgment | Description |
|---|---|
G ctx |
G is a well-formed context |
Inh T |
T is inhabitable (may occur on the right side of a typing judgment) |
Univ T |
Tis a universe (inhabitable, and every t:T is also inhabitable) |
t1 = t2 [:T] |
t1 is equal to t2 (under optional type T) |
t1 ~> t2 |
t1 simplifies to t2 |
t :=> T |
The principal type of t is T |
t :<= T |
t checks against the given type T |
T1 <: T2 |
T1 is a subtype of T2 |
Prov T |
T is inhabited |
In general, whenever a constant c : T [= d] is parsed, the solver will check the following judgments:
Inh Td :<= TThe classes corresponding to these judgements and the tactics used to check them are described here.