Commit 31ac0c56 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

some fixes

parent 814354bc
......@@ -281,10 +281,11 @@ rules, because one branch is already unreachable and retyping only occurs with s
\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(e).\ \Gamma_j(y)\leq\Gamma_i(y)\}\\
\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 J_i\text{ s.t. }
\Gamma_j(x)\land\Gamma_k(x)\neq\varnothing\\\text{ and }
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
)})
......@@ -295,6 +296,11 @@ 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.
\subsection{Backward typing rules}
\begin{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