[−][src]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.