[−][src]Module minitt::type_check

Type checking: the four type checking functions -- checkI, checkD, check and checkT.

Depends on modules syntax, normal, reduce and read_back.

Functions

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.

Type Definitions

Gamma

Gamma in Mini-TT.
By doing this we get lookupG in Mini-TT for free.