[−][src]Module minitt::check::tcm

Type-Checking Monad: context, state and error.

Typing context (Gamma) and its updater, the type-checking error and its pretty-printer

Depends on module syntax.

Structs

TCS	Type-Checking State ~~, not "Theoretical Computer Science"~~. This is not present in Mini-TT.

TCE	Type-Checking Error.

update_gamma	Move version of `upG` in Mini-TT. `Gamma \|- p : t = u => Gamma’` `Cow` is used to simulate immutability.
update_gamma_borrow	Borrow version of `upG` in Mini-TT.
update_gamma_lazy	Lazy version of `upG` in Mini-TT.

Gamma	`Gamma` in Mini-TT. By aliasing `BTreeMap` to `Gamma`, 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.