Commit d217479a authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix

parent 06614460
......@@ -546,7 +546,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetNoRefine]
{
\Gamma\avdash{\Gammap}\ct a:\Node(t_1,\Gamma_1)\\
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\Gamma_1)\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
x\not\in\dom\Gammap\text{ or }\Gamma_1'(x)\leq \Gammap(x)\\
\Gamma_1'\avdash{\Gammap\setminus\{x\}}{\ct[\letexp x a {[]}]} e : \tree
......@@ -558,7 +558,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\\
\Infer[LetRefine]
{
\Gamma\avdash{\Gammap}\ct a:\{(t_1,\Gamma_1)\}\\
\Gamma\avdash{\Gammap}\ct a:\Leaf(t_1,\Gamma_1)\\
\Gamma_1'=\Gamma_1\subst{x}{\Gamma_1(x)\land t_1}\\
\Gamma_1'\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_1'\subst{x}{\Gamma(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
......
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