Type checking: the four type checking functions -- checkI
, checkD
, check
and checkT
.
Depends on modules syntax
, normal
, reduce
and read_back
.
check | check in Mini-TT.
|
check_declaration | checkD in Mini-TT.
Check if a declaration is well-typed and update the context.
|
check_infer | checkI in Mini-TT.
Type inference rule. More inferences are added here (maybe it's useful?).
|
check_type | checkT in Mini-TT.
Check if an expression is a well-typed type expression.
|
update_gamma | upG in Mini-TT.
Gamma |- p : t = u => Gamma’
However, since Rust is an imperative language, we use mutable reference instead of making it
monadic.
|
Gamma | Gamma in Mini-TT.
By doing this we get lookupG in Mini-TT for free.
|
GammaRaw | |
TCM | G in Mini-TT.
Type-Checking Monad.
|