Module voile::check::decl

Declaration relevant checking. $$ \newcommand{\checkD}[0]{\vdash_\texttt{d}} \newcommand{\GcheckD}[0]{\Gamma \checkD} \GcheckD D\ \textbf{ok} $$

Depends on expr.

Functions

check_decl	Checking one declaration. $$ \newcommand{\cdecl}[2]{#1 \vdash_\texttt{d} #2 \ \textbf{ok}} \newcommand{\Gcdecl}[1]{\cdecl{\Gamma}{#1}} \newcommand{\infer}[3]{#1 \vdash_\texttt{i} #2 \Leftarrow #3} \newcommand{\xx}[0]{\texttt{x}} \newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4} \newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}} \newcommand{\ty}[0]{\tau} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \cfrac{}{\cdecl{}{}} \quad \cfrac{}{ \infer{ \Gamma, \textbf{val } \xx' : \cA }{\xx'}{\cA} } \quad \cfrac{ \Gtyck{A}{\ty}{\cA} \quad \cdecl{ \Gamma, \textbf{val } \xx' : \cA }{D} }{ \Gcdecl{\textbf{val } \xx' : A; D} } \\ \space \\ \cfrac{ \tyck{ \Gamma, \xx' : \cA }{a}{\cA}{\alpha} \quad \cdecl{ \Gamma, \textbf{val } \xx' : \cA, \textbf{let } \xx' = \alpha }{D} }{ \cdecl{ \Gamma, \textbf{val } \xx' : \cA }{\textbf{let } \xx' = a; D} } $$
check_decls	Checking a list of declarations.
inline_metas
require_local_emptiness
unimplemented_to_glob