[−][src]Function minitt::check::decl::check_recursive_declaration
pub fn check_recursive_declaration(
index: u32,
tcs: TCS<'_>,
declaration: Declaration
) -> TCM<Gamma<'_>>
$$
\frac{\rho,\Gamma\vdash_l A
\quad \Gamma\vdash p:t=[\textsf{x}_l]\Rightarrow \Gamma_1
\quad (\rho,p=[\textsf{x}_l]),\Gamma\vdash_{l+1} M\Leftarrow t
\quad \Gamma\vdash p:t=v\Rightarrow \Gamma_2}
{\rho,\Gamma\vdash_l \textsf{rec}\ p:A=M\Rightarrow \Gamma_2}
$$
$$
\dbinom{t=⟦A⟧\rho,}{v=⟦M⟧(\rho,\textsf{rec}\ p:A=M)}
$$
Extracted from checkD
in Mini-TT.
This part deals with recursive declarations, but without prefixed parameters.