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

small fix in implem

parent ac767280
......@@ -679,7 +679,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\Gamma_\circ\bvdash{a}{\Gammap(x)}\{\Gamma_i\}_{i\in I}\\
\forall i\in I.\ \Gamma_\circ\subst{x}{\Gamma_\circ(x)\land\Gammap(x)}\avdash{(\Gammap\land\Gamma_i)\setminus\{x\}}{[]} \ct[\letexp x a e] : \tree_i}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma,\{(\{\}, \tree_i)\}_{i\in I})
\Gamma\avdash\Gammap\ct\letexp x a e : \Node(\Gamma_\circ,\{(\{\}, \tree_i)\}_{i\in I})
}
{ }
\end{mathpar}
......
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