Module voile::check

Type-Checking module.

Modules

decl	Declaration relevant checking. $$ \newcommand{\checkD}[0]{\vdash_\texttt{d}} \newcommand{\GcheckD}[0]{\Gamma \checkD} \GcheckD D\ \textbf{ok} $$
eval	Tooling functions that depends on neither decl nor expr. $$ \llbracket a \rrbracket = \alpha $$
expr	Expression/Type relevant checking. $$ \newcommand{\tyck}[0]{\vdash_\texttt{c}} \newcommand{\Gtyck}[0]{\Gamma \tyck} \newcommand{\infer}[0]{\vdash_\texttt{i}} \newcommand{\Ginfer}[0]{\Gamma \infer} \Ginfer a \Rightarrow o \quad \Gtyck a:m \Rightarrow o \quad \Gamma \vdash A <: B $$
monad	Type-checking monad is a Result<State, Error>. $$ \newcommand{\xx}[0]{\texttt{x}} \Gamma \quad \Gamma(\xx)=o $$
unify	Meta variable solving, term (definitional) equality comparison. $$ \Gamma \vdash A \simeq B $$

Functions

check_decls	Checking a list of declarations.
compile_cons	Evaluate a single constructor as a lambda.
inline_metas