Commit 999343fa authored by Mickael Laurent's avatar Mickael Laurent
Browse files

update abs rule

parent 09644e84
......@@ -280,17 +280,12 @@ rules, because one branch is already unreachable and retyping only occurs with s
\begin{mathpar}
\Infer[Abs]
{\Gamma,(x:s)\avdash{\Gammap}{\ct} e:\{(t_i,\Gamma_i)\}_{i\in I}\\
\forall i\in I.\ J_i=\{j\,\alt\,j\in I\text{ s.t. }
\forall y\in\fv(\lambda x:s.e).\ \Gamma_i(y)\leq\Gamma_j(y)\}\\
\forall i\in I.\ u_i = \bigwedge_{j\in J_i}(\arrow{\Gamma_j(x)}{(
t_j\vee\bigvee_{\substack{k\in I\text{ s.t. }
\forall y\in\fv(e).\ \Gamma_j(y)\land\Gamma_k(y)\neq\varnothing\\
\text{ and }
\exists y\in\bv(e).\ \Gamma_k(y)\not\leq\Gamma_j(y)}
} t_k
)})
\{(t'_i,\Gamma'_i)\}_{i\in I'} = \{ (\textstyle\bigvee_{j\in I\text{ s.t. }\Gamma_i\setminus\bv(e)\equiv\Gamma_j\setminus\bv(e)} t_j,\ \Gamma_i\setminus\bv(e)) \alt i\in I \}\\
\forall i\in I'.\ t''_i = \textstyle\bigvee_{j\in I'\text{ s.t. } \Gamma'_i\land\Gamma'_j\neq\bot}t'_j
}
{\Gamma\vdash\lambda x:s.e: \{(u_i,\Gamma_i)\,\alt\,i\in I\}}
{\Gamma\vdash\lambda x:s.e: \{(
\textstyle\bigwedge_{j\in I'\text{ s.t. }\Gamma_i\setminus\{x\}\equiv\Gamma_j\setminus\{x\}} \arrow{\Gamma'_j(x)}{t''_j},\
\Gamma'_i\setminus\{x\})\,\alt\,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