Commit db23b332 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added comment

parent eb6838d1
......@@ -191,16 +191,16 @@ Finally, we add the following typing rules:
\begin{mathpar}
\Infer[Record]
{~}
{\Gamma \vdash \crecord {}:\crecord {}}
{}
\Infer[Proj]
{\Gamma \vdash e:t\and t\leq\orecord {}}
{\Gamma \vdash e.\ell:\proj \ell {t}}
{e.\ell\not\in\dom\Gamma}
\Infer[Record]
{}
{\Gamma \vdash \crecord {}:\crecord {}}
{}
\Infer[Delete]
{\Gamma \vdash e:t\and t\leq\orecord {}}
{\Gamma \vdash \recdel e \ell: \recdel t \ell}
......
......@@ -151,3 +151,4 @@ then
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}\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*}
\beppe{Explain, especially the last one}
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