[−][src]Module minitt::check::expr
Expression checker: infer, instance-of check, normal-form comparison, subtyping, etc.
Depends on modules syntax
, read_back
and tcm
.
Functions
check |
|
check_fallback | Fallback rule of instance check. |
check_infer |
|
check_level | Level comparison |
check_merge_type | To reuse code that checks if a merge expression is well-typed between |
check_sum_type | To reuse code that checks if a sum type is well-typed between |
check_telescoped | To reuse code that checks if a sigma or a pi type is well-typed between |
check_type |
|