Commit b7bc06c3 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add domain checl to the App rule

parent 1589fca0
......@@ -138,7 +138,8 @@ We define the following algorithmic system (we deduce at most one type for every
{
\Gamma \vdash e_1: t_1 \\
\Gamma\vdash e_2: t_2\\
t_1 \leq \Empty \to \Any
t_1 \leq \Empty \to \Any\\
t_2 \in \dom {t_1}
}
{ \Gamma \vdash {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
......
......@@ -390,7 +390,8 @@ just simple types.
{
\Gamma \vdash e_1: t_1 \\
\Gamma\vdash e_2: t_2\\
t_1 \leq \Empty \to \Any
t_1 \leq \Empty \to \Any\\
t_2 \in \dom {t_1}
}
{ \Gamma \vdash {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
......
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