Commit 733b7652 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

deleted footnote 9

parent cbbe1e7e
......@@ -32,7 +32,10 @@ $\ell \in \Labels$ to the type $t$ (all the $\ell_i$'s must be
distinct). Quasi constant functions are the internal representation of
record types in CDuce. These are not visible to the programmer who can use
only two specific forms of quasi constant functions, open record types and closed record types, provided by the
following syntactic sugar and that form the \emph{record types} of our language\footnote{Note that in the definitions ``$\ldots{}$'' is meta-syntax to denote the presence of other fields while in the open records ``{\large\textbf{..}}'' is the syntax that distinguishes them from closed ones.}
following syntactic sugar and that form the \emph{record types} of our language%
\iflongversion%
\footnote{Note that in the definitions ``$\ldots{}$'' is meta-syntax to denote the presence of other fields while in the open records ``{\large\textbf{..}}'' is the syntax that distinguishes them from closed ones.}
\fi
\begin{itemize}[nosep]
\item $\crecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Undef}$ (closed records).
\item $\orecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Any \vee \Undef}$ (open records).
......@@ -66,7 +69,8 @@ Expressions are then typed by the following rules (already in algorithmic form).
{\Gamma \vdash e_1:t_1\and t_1\leq\orecord {\!\!} \and \Gamma \vdash e_2:t_2}
{\Gamma \vdash \recupd{e_1}{\ell}{e_2}: t_1 + \crecord{\ell=t_2}}
{\recupd{e_1\!\!}{\!\!\ell}{e_2} \not\in\dom\Gamma}
\vspace{-2mm}\\
\end{mathpar}
\begin{mathpar}\vspace{-4mm}\\
\Infer[Delete]
{\Gamma \vdash e:t\and t\leq\orecord {\!\!}}
{\Gamma \vdash \recdel e \ell: \recdel t \ell}
......
......@@ -150,7 +150,7 @@ core and the use of subtyping, given by the following typing rules:\vspace{-1mm}
% {\Gamma\vdash \ite {e} t {e_1}{e_2}: t'}
% { }
\end{mathpar}
\begin{mathpar}\vspace{-4mm}\\
\begin{mathpar}
\Infer[Sel]
{\Gamma \vdash e:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_i e:t_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