[−][src]Module voile::check
Type-Checking module.
Modules
| decl | Declaration relevant checking. |
| eval | Tooling functions that depends on neither |
| expr | $$ \newcommand{\xx}[0]{\texttt{x}} \newcommand{\istype}[0]{\vdash_\texttt{t}} \newcommand{\Gistype}[0]{\Gamma \istype} \newcommand{\tyck}[0]{\vdash_\texttt{c}} \newcommand{\Gtyck}[0]{\Gamma \tyck} \newcommand{\infer}[0]{\vdash_\texttt{i}} \newcommand{\Ginfer}[0]{\Gamma \infer} \newcommand{\subtype}[0]{\vdash_{<:}} \newcommand{\Gsubtype}[0]{\Gamma \subtype} \newcommand{\ty}[0]{\textsf{Type}} \newcommand{\Sum}[0]{\texttt{Sum}\ } \newcommand{\merge}[0]{\texttt{merge}} \newcommand{\inst}[0]{\texttt{inst}} \newcommand{\ctor}[0]{\texttt{cons}\ } \newcommand{\app}[0]{\texttt{app}} \newcommand{\first}[0]{\texttt{first}} \newcommand{\second}[0]{\texttt{second}} \Gistype a \Rightarrow o \quad \Ginfer a \Rightarrow o \quad \Gtyck a:m \Rightarrow o $$ Expression/Type relevant checking. |
| monad | $$
\newcommand{\xx}[0]{\texttt{x}}
\Gamma
\quad
\Gamma(\xx)=o
$$
Type-checking monad is a |
| unify | Meta variable solving, term (definitional) equality comparison. |
Functions
| check_decls | |
| compile_cons | |
| compile_variant | |
| expand_meta | Require |