[−][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.

Enums

TCE	Type-Checking Error.

check	`check` in Mini-TT. However, telescope and gamma are preserved for REPL use.
check_contextual	For REPL: check an expression under an existing context
check_declaration	`checkD` in Mini-TT. Check if a declaration is well-typed and update the context.
check_declaration_main	Similar to `checkMain` in Mini-TT, but for a declaration.
check_infer	`checkI` in Mini-TT. Type inference rule. More inferences are added here (maybe it's useful?).
check_infer_contextual	For REPL: infer the type of an expression under an existing context
check_main	`checkMain` in Mini-TT.
check_type	`checkT` in Mini-TT. Check if an expression is a well-typed type expression.
default_state	Empty `TCS`.
update_gamma	`upG` in Mini-TT. `Gamma \|- p : t = u => Gamma’` `Cow` is used to simulate immutability.

Gamma	`Gamma` in Mini-TT. By doing this we get `lookupG` in Mini-TT for free.
GammaRaw	Type-Checking context. Name as key, type of the declaration as value.
TCM	`G` in Mini-TT. Type-Checking Monad.
TCS	Type-Checking State~~, not "Theoretical Computer Science"~~. This is not present in Mini-TT.