Commit 09644e84 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

some fixes

parent 31ac0c56
......@@ -297,9 +297,9 @@ rules, because one branch is already unreachable and retyping only occurs with s
TODO: Check abs rule
TODO: The current environments returned by the typing rules are
not adapted at all to type lambda abstractions. It shouldn't contain
info about bound variables, and the type associated with a given environment
should cover all the cases for this environment.
not adapted at all to type lambda abstractions. The type associated
with a given environment should cover all the cases for this environment.
==> Need for the other refinement type system
\subsection{Backward typing rules}
......@@ -347,7 +347,7 @@ should cover all the cases for this environment.
\forall i\in I.\ \Gamma_2^i = \subst{x_2}{t_i\land t'}\\
\forall i\in I.\ u_i\leq\arrow{(t_i\land t')}{s_i}}
{
\Gamma\bvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i, \Gamma_{1}^i\land\Gamma_{2}^i)\}
\Gamma\bvdash {(x_1\ x_2)} {t} \bigcup_{i\in I}\{(s_i\land t, \Gamma_{1}^i\land\Gamma_{2}^i)\}
}
{ }
\\
......
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