Function minitt::check::expr::check_infer

pub fn check_infer(index: u32, tcs: TCS, expression: Expression) -> TCM<Value>

$$ \frac{\Gamma(x)\rightarrow t} {\rho,\Gamma\vdash_l x\Rightarrow t} \quad \frac{\rho,\Gamma\vdash_l M \Rightarrow \Pi\ t\ g \quad \rho,\Gamma\vdash_l N\Leftarrow t} {\rho,\Gamma\vdash_l M\ N \Rightarrow \textsf{inst}\ g(⟦N⟧\rho)} $$ $$ \frac{}{\rho,\Gamma\vdash_l 0 \Rightarrow \textbf{1}} \quad \frac{}{\rho,\Gamma\vdash_l \textbf{1} \Rightarrow \textsf{U}} $$ $$ \frac{\rho,\Gamma\vdash_l M\Rightarrow \Sigma\ t\ g} {\rho,\Gamma\vdash_l M.1\Rightarrow t} \quad \frac{\rho,\Gamma\vdash_l M\Rightarrow \Sigma\ t\ g} {\rho,\Gamma\vdash_l M.2 \Rightarrow \textsf{inst}\ g((⟦M⟧\rho).1)} $$ checkI in Mini-TT.
Type inference rule. More inferences are added here (maybe it's useful?).