[−][src]Function minitt::check::tcm::update_gamma
pub fn update_gamma<'a>(
gamma: Gamma<'a>,
pattern: &Pattern,
type_val: Value,
body: Value
) -> TCM<Gamma<'a>>
Move version of upG
in Mini-TT.
$$
\frac{}{\Gamma \vdash x:t=v\Rightarrow \Gamma,x:t}
\quad
\frac{}{\Gamma \vdash _:t=v\Rightarrow \Gamma}
$$
$$
\frac{\Gamma \vdash p_1:t_1=v.1 \Rightarrow \Gamma_1
\quad \Gamma \vdash p_2:\textsf{inst}\ g(v.1)=v.2 \Rightarrow \Gamma_2}
{\Gamma \vdash (p_1,p_2):\Sigma\ t_1\ g=v\Rightarrow \Gamma_2}
$$
Cow
is used to simulate immutability.