[−][src]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.