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{\recordext}[2]{\record{#1 \mid #2}} \newcommand{\recExt}[1]{\mid #1} \newcommand{\variant}[1]{\textbf{Sum}\ { #1 }} \newcommand{\record}[1]{\textbf{Rec}\ { #1 }} \newcommand{\nocases}[0]{\textbf{whatever}} \newcommand{\case}[4]{\textbf{case}\ #1\ #2: #3\ \textbf{or}\ #4} \newcommand{\variantext}[2]{\variant{#1 \mid #2}} \newcommand{\ctyLab}[0]{\gamma} \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 } } \\ \space \\ \cfrac{ \Gtyck{B}{\ty}{\cB} \quad \Gcheval{b}{\cB} }{ \cfrac{ \Gcheval{a}{\record{\ctyLab}} }{ \Gcheval{ \{ n = b\recExt{a} \} }{ \record{n : \cB, \ctyLab} } } \quad \cfrac{ \Gcheval{a}{[k]} }{ \Gcheval{ \{ n = b\recExt{a} \} }{ [\recordext{n : \cB}{k}] } } } \\ \space \\ \cfrac{ \Gtyck{A}{\ty}{\cA} }{ \Gcheval{\nocases}{ \piTy{\xx : \variant{} . \cA} } \quad \cfrac{ \Gtyck{a}{\variant{}}{\alpha} }{ \Gtyck{\nocases\ a}{\cA}{\alpha} } } \\ \space \\ \cfrac{ \cheval{\Gamma,\xx : \cA_1}{b}{\cB} \quad \Gtyck{A_1}{\ty}{\cA_1} }{ \cfrac{ \Gcheval{a}{\piTy{\xx : \variant{\ctyLab} . \cB}} }{ \Gcheval{ (\case{n}{\xx}{b}{a}) }{ \piTy{\xx : \variant{n : \cA_1, \ctyLab} . \cB} } } \quad \cfrac{ \Gcheval{a}{\piTy{\xx : [k] . \cB}} }{ \Gcheval{ (\case{n}{\xx}{b}{a}) }{ \piTy{\xx : [\variantext{n : \cA_1}{k}] . \cB} } } } $$