Commit 207b925d authored by Mickael Laurent's avatar Mickael Laurent
Browse files

fix the Abs- rule

parent 65ed1d06
......@@ -194,9 +194,9 @@ system, that is, the fact that $\lambda$-abstractions can have negated
arrow types, as long as these negated types do not make the type deduced for the function empty:\vspace{-1mm}
\begin{mathpar}
\Infer[Abs-]
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }\vspace{-3mm}
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\end{mathpar}
%\beppe{I have doubt: is this safe or should we play it safer and
% deduce $t\wedge\neg(t_1\to t_2)$? In other terms is is possible to
......
......@@ -43,7 +43,7 @@
\Infer[Abs-]
{\Gamma \vdash \lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:t}
{ \Gamma \vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\neg(t_1\to t_2) }
{ (t\wedge\neg(t_1\to t_2))\not\simeq\Empty }
{ ((\wedge_{i\in I}\arrow {s_i} {t_i})\wedge\neg(t_1\to t_2))\not\simeq\Empty }
\\
\Infer[Case]
{\Gamma\vdash e:t_0\\
......
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