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.