Commit 2114badf authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 7e74089f de975750
......@@ -39,7 +39,7 @@
\Gamma\vdash\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle \bigwedge_{i\in I}\arrow {s_i} {t_i}
}
{ }
\qquad
\\
\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) }
......@@ -743,6 +743,8 @@
\end{description}
\end{proof}
\pagebreak
\subsection{Operator $\worra {} {}$}\label{app:worra}
In this section, we will use the algorithmic definition of $\worra {} {}$ and show that it is equivalent to its
......@@ -1616,4 +1618,5 @@
\end{description}
\end{description}
\end{proof}
\ No newline at end of file
\newpage
\ No newline at end of file
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