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

small fix in implem

parent c4be3dba
......@@ -653,7 +653,7 @@ rules, because one branch is already unreachable and retyping only occurs with s
\forall i\in I'.\ \forall j\in J_i.\ x\in\dom{\Gamma_{i,j}'} \Rightarrow (\Gamma_i'\land\Gamma_{i,j}')\setminus\{x\} \fvdash{a}{\Gamma_{i,j}'(x)} \{\Gamma_{i,j,k}'\}_{k\in K_j}\\
\forall i\in I'.\ \forall j\in J_i.\ x\not\in\dom{\Gamma_{i,j}'} \Rightarrow \{\Gamma_{i,j,k}'\}_{k\in K_j} = \{\{\}\} \\
\tree''= \tree'\text{ with, for each } i\in I' \text{, the label } \{\Gamma_{i,j}'\}_{j\in J_i}
\text{ replaced by } \{(\Gamma_{i,j,k}'\land\Gamma_{i,j}')\setminus\{x\}\,\alt\,j\in J_i, k\in K_j\}
\\\\\text{ replaced by } \{(\Gamma_{i,j,k}'\land\Gamma_{i,j}')\setminus\{x\}\,\alt\,j\in J_i, k\in K_j\}
}
{
\Gamma\avdash\Gammap\ct\letexp x a e : \tree''
......
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