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

fix app rule & 'square' operator

parent f727aced
......@@ -194,12 +194,7 @@ Finally, we add the following typing rules:
{\Gamma \vdash e.\ell:\proj \ell {t}}
{e.\ell\not\in\dom\Gamma}
\Infer[Open]
{}
{\Gamma \vdash \orecord {}:\orecord {}}
{}
\Infer[Closed]
\Infer[Record]
{}
{\Gamma \vdash \crecord {}:\crecord {}}
{}
......
......@@ -120,11 +120,11 @@ We define the following algorithmic system (we deduce at most one type for every
\\
\Infer[App]
{
\Gamma \vdash e_1: t_1 \to t \\
\Gamma \vdash e_1: t_1 \\
\Gamma\vdash e_2: t_2\\
t_2\leq t_1
t_1 \leq \Empty \to \Any
}
{ \Gamma \vdash {e_1}{e_2}: t }
{ \Gamma \vdash {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
......@@ -145,5 +145,5 @@ then
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
t\circ s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\bigvee_{\{p\in P_i\alt s\wedge t_p\not=\varnothing\}}s_p
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigvee_{\{p\in P_i\alt s\wedge t_p\not=\varnothing\}}s_p \setminus \bigvee_{\{p\in P_i\alt s\wedge t_p=\varnothing\}}s_p \right)
\end{eqnarray*}
......@@ -388,11 +388,11 @@ just simple types.
\\
\Infer[App]
{
\Gamma \vdash e_1: t_1 \to t \\
\Gamma \vdash e_1: t_1 \\
\Gamma\vdash e_2: t_2\\
t_2\leq t_1
t_1 \leq \Empty \to \Any
}
{ \Gamma \vdash {e_1}{e_2}: t }
{ \Gamma \vdash {e_1}{e_2}: t_1 \circ t_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[If]
......
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