Commit 1632c038 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

let rule in progress

parent ca61d22c
......@@ -252,9 +252,9 @@ rules, because one branch is already unreachable and retyping only occurs with s
x\in\dom\Gamma\Rightarrow t=\Gamma(x)\\x\not\in\dom\Gamma\Rightarrow t=\Any\\
x\in\dom\Gamma'\Rightarrow t'=\Gamma'(x)\\x\not\in\dom\Gamma'\Rightarrow t'=\Any\\
\Gamma\avdash\Gammap\ct a:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ t_i\land t\leq t' \Rightarrow \Gamma_i\subst{x}{t_i\land t}\avdash{\Gammap}{\ct[\letexp x a {[]}]} e : S_i\\
\forall i\in I.\ t_i\land t\leq t' \Rightarrow \Gamma_i\subst{x}{t_i\land t}\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : S_i\\
\forall i\in I.\ t_i\land t\not\leq t' \Rightarrow\Gamma_i\land\Gamma'\bvdash{a}{t'\land t\land t_i}\{(t_j,\Gamma_j)\}_{j\in J_i}\\
\forall i\in I.\ \forall j\in J_i.\ \Gamma_i\subst{x}{t_j}\avdash{\Gammap_j}{[]} \ct[\letexp x a e] : S_j}
\forall i\in I.\ \forall j\in J_i.\ \Gamma_i\subst{x}{t_j}\avdash{\Gammap_j\setminus\{x\}}{[]} \ct[\letexp x a e] : S_j}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \textstyle\bigcup S_i \cup \textstyle\bigcup\bigcup S_j
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment