[−][src]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 |
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 |
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 |