Function minitt::check::expr::check

pub fn check(
    index: u32, 
    tcs: TCS<'_>, 
    expression: Expression, 
    value: Value
) -> TCM<TCS<'_>>

$$ \frac{\rho,\Gamma\vdash_l M\Leftarrow ⟦A_i⟧v} {\rho,\Gamma\vdash_l c_i \ M \Leftarrow \textsf{Sum} \lang c_1\ A_1 | \dots | c_n\ A_n,v \rang} $$ $$ \frac{}{\rho,\Gamma\vdash_l 0 \Leftarrow \textbf{1}} \quad \frac{}{\rho,\Gamma\vdash_l \textbf{1} \Leftarrow \textsf{U}} $$ $$ \frac{\rho,\Gamma\vdash_l M_1\Leftarrow \Pi(⟦A_1⟧v)(g \circ c_1) \dots \rho,\Gamma\vdash_l M_n\Leftarrow \Pi(⟦A_n⟧v)(g \circ c_n)} {\rho,\Gamma\vdash_l \textsf{fun}(c_1\rightarrow M_1 | \dots | c_n \rightarrow M_n) \Leftarrow \Pi(\textsf{Sum}\lang c_1:A_1 | \dots | c_n:A_n,v \rang)g} $$ $$ \frac{\rho,\Gamma\vdash_l D\Rightarrow \Gamma_1 \quad (\rho,\Gamma),\Gamma_1\vdash_l M\Leftarrow t} {\rho,\Gamma\vdash_l D; M\Leftarrow t} $$ $$ \frac{\rho,\Gamma\vdash_l M\Rightarrow t' \quad \textsf{R}_l\ t =\textsf{R}_l\ t'} {\rho,\Gamma\vdash_l M\Leftarrow t} (\textnormal{If other rules are not applicable}) $$ $$ \dots (\textnormal{There are too many, please checkout the original paper for more}) $$ check in Mini-TT.
However, telescope and gamma are preserved for REPL use.