Function voile::check::expr::check

fn check(tcs: TCS, expr: &Abs, expected_type: &Val) -> ValTCM

Check an abstract term against an expected type and produce a well-typed term. $$ \newcommand{\tyck}[4]{#1 \vdash_\texttt{c} #2 : #3 \Rightarrow #4} \newcommand{\Gtyck}[3]{\tyck{\Gamma}{#1}{#2}{#3}} \newcommand{\eval}[1]{\llbracket #1 \rrbracket} % {\texttt{eval}(#1)} \newcommand{\cheval}[3]{#1 \vdash_\texttt{e} #2 \Rightarrow #3} \newcommand{\Gcheval}[2]{\cheval{\Gamma}{#1}{#2}} \newcommand{\subt}[0]{<:} \newcommand{\xx}[0]{\texttt{x}} \newcommand{\ty}[0]{\tau} \newcommand{\piTy}[1]{\Pi \langle #1 \rangle} \newcommand{\sigTy}[1]{\Sigma \langle #1 \rangle} \newcommand{\cA}[0]{\mathcal A} \newcommand{\cB}[0]{\mathcal B} \cfrac{ \Gtyck{a}{\cA}{\alpha} \quad \Gtyck{b}{\cB[\xx := \alpha]}{\beta} }{ \Gcheval{a, b}{\sigTy{\xx : \cA . \cB}} } \quad \cfrac{ \tyck{\Gamma, \xx : \cB}{a}{\cA}{\alpha} }{ \Gtyck{ \lambda \xx. \alpha}{\piTy{\xx : \cB . \cA} }{ \lambda \langle \xx . \alpha \rangle } } $$