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

wording

parent 0aaf1a6a
......@@ -675,10 +675,10 @@ application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
the deduction system for $\vdashp$: case \eqref{uno} corresponds
to the application of \Rule{PEps}; case \eqref{due} implements \Rule{Pappl}
straightforwardly; the implementation of rule \Rule{PAppR} is subtler:
instead of finding the best $t_1$ to subtract (by intersection) to the
static type of the argument, \eqref{tre} finds directly this type by
instead of finding the best $t_1$ to subtract (by intersection) from the
static type of the argument, \eqref{tre} finds directly the best type for the argument by
applying the operator $\worra{}{}$ to the static types of the function
and of the application. The remaining (\ref{quattro}--\ref{sette})
and the refined type of the application. The remaining (\ref{quattro}--\ref{sette})
cases are the straightforward implementations of the rules
\Rule{PPairL}, \Rule{PPairR}, \Rule{PFst}, and \Rule{PSnd},
respectively.
......
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