[−][src]Function minitt::check::expr::check_telescoped
pub fn check_telescoped(
index: u32,
tcs: TCS,
first: Typed,
second: Expression
) -> TCM<(Level, TCS)>
$$
\frac{\rho,\Gamma\vdash_l A
\quad \Gamma\vdash p:⟦A⟧\rho=[\textsf{x}_l]\Rightarrow\Gamma_1
\quad (\rho,p=[\textsf{x}_l]), \Gamma_1\vdash_{l+1}B}
{\rho,\Gamma\vdash_l (\Pi /\Sigma) \ p:A.B}
$$
To reuse code that checks if a sigma or a pi type is well-typed between check_type
and check