Module voile::check

Type-Checking module.

Modules

decl	Declaration relevant checking.
expr	Expression/Type relevant checking.
monad
util	Tooling functions that depends on neither decl nor expr.

Functions

check	$$ \newcommand\U{\textsf{Type}} \cfrac{i < j}{\Gamma \vdash \U_i : \U_j \rightsquigarrow \U_i} \quad \cfrac{}{\Gamma \vdash\bot:\U_i \rightsquigarrow \bot_i} \newline \cfrac{\Gamma \vdash a:A \quad \Gamma,a:A \vdash b:B(a)} {\Gamma \vdash (a,b):\Sigma (a:A).B(a) \rightsquigarrow (a,b)} $$ Abstract Term -> Core Term under an expected type.
check_decl
check_decls
check_main
check_subtype	check if type1 is subtype of type2
check_type	Check if an expression is a valid type expression.
infer	$$ \newcommand\U{\textsf{Type}} \newcommand\G[2]{\Gamma \vdash #1 : #2} \cfrac{}{\G{\U_i}{\U_{i+1}}} \quad \cfrac{}{\G{[n]}{\textsf{type}(\Gamma, n)}} \newline \cfrac{\G{a}{A} \quad \G{b}{B}}{\G{(a,b)}{\Sigma A.B}} \quad \cfrac{\G{a}{\Sigma A.B}}{\G{a\textsf{.1}}{A}} $$ Infer type of a value.
unsafe_compile	Ensure abs is well-typed before invoking this, otherwise this function may panic or produce ill-typed core term.