[−][src]Module minitt::check
Type checking: everything related to type-checking.
This module includes:
- Normal form and read-back functions
- The four type checking functions --
checkI
,checkD
,check
andcheckT
. - (extended) (sub)typing rules
Depends on module syntax
.
Modules
decl | Declaration checker: for prefix parameters, simple declarations and recursive declarations. |
expr | Expression checker: infer, instance-of check, normal-form comparison, subtyping, etc. |
read_back | Read back: read back functions and normal form definitions. |
subtype | Subtyping check: fallback rules of "instance of" checks: infer the expression's type and check if it's the subtype of the expected type. |
tcm | Type-Checking Monad: context, state and error. |
Functions
check_contextual | For REPL: check an expression under an existing context |
check_declaration_main | Similar to |
check_infer_contextual | For REPL: infer the type of an expression under an existing context |
check_main |
|