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 in Mini-TT. However, telescope and gamma are preserved for REPL use.
check_fallback	Fallback rule of instance check. First infer the expression type, then do subtyping comparison.
check_infer	checkI in Mini-TT. Type inference rule. More inferences are added here (maybe it's useful?).
check_sum_type	To reuse code that checks if a sum type is well-typed between check_type and check
check_telescoped	To reuse code that checks if a sigma or a pi type is well-typed between check_type and check
check_type	checkT in Mini-TT. Check if an expression is a well-typed type expression.