[−][src]Function minitt::check::decl::check_lift_parameters
pub fn check_lift_parameters<'a>(
index: u32,
tcs: TCS<'a>,
parameters: Vec<Typed>,
check_body: impl FnOnce(TCS<'a>) -> TCM<LiftState<'a>>
) -> TCM<LiftState<'a>>
$$
\frac{\rho \ \texttt{empty} \quad T:\textsf{U} \quad a:T}
{\textnormal{checkLiftD}(a,T,\rho)}
$$
$$
\frac{\rho\equiv[(v,T)::\rho'] \quad T:\textsf{U}
\quad v:T\vdash R:\textsf{U}
\quad \Gamma,v:T\vdash\textnormal{checkLiftD}(a,R,\rho')}
{\Gamma\vdash\textnormal{checkLiftD}(\lambda v.a,\Pi (v:T).R,\rho)}
$$
This is an extension, it's not present in Mini-TT.
Lift all these parameters
into the context.
Returning TCS
to reuse the variable.
check_body
is supposed to return signature
, body
and tcs
.