Function minitt::check::decl::check_simple_declaration

pub fn check_simple_declaration(
    index: u32, 
    tcs: TCS, 
    pattern: Pattern, 
    signature: Expression, 
    body: Expression
) -> TCM<Gamma>

$$ \frac{\rho,\Gamma\vdash_l A \quad \rho,\Gamma\vdash_l M\Leftarrow t \quad \Gamma\vdash p:t=⟦M⟧\rho\Rightarrow \Gamma_1} {\rho,\Gamma\vdash_l p:A=M\Rightarrow \Gamma_1} $$ $$ (t=⟦M⟧\rho) $$ Extracted from checkD in Mini-TT.
This part deals with non-recursive declarations, but without prefixed parameters.