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


parent 55bc3669
......@@ -583,7 +583,7 @@ its domain and the type of the application is more complicated and needs the ope
\apply t s & = &\,\min \{ u \alt t\leq s\to u\}
\worra t s & = &\,\min\{u \alt t\circ(\dom t\setminus u)\leq \neg s\}\label{worra}
%In short, $\dom t$ is the largest domain of any single arrow that
%subsumes $t$, $\apply t s$ is the smallest domain of an arrow type
%that subsumes $t$ and has domain $s$ and $\worra t s$ was explained
......@@ -656,7 +656,7 @@ in the definition are defined).\footnote{Note that the definition is
this is defined for all $\varpi$ since the first premisses of
\Rule{Case\Aa} states that $\Gamma\vdash e:\ts_0$ (and this is
possible only if we were able to deduce under the hypothesis
$\Gamma$ the type of every occurrence of $e$.)}
$\Gamma$ the type of every occurrence of $e$.)\vspace{-3mm}}
Each case of the definition of the $\constrf$ function corresponds to the
application of a logical rule (\emph{cf.} Footnote~\ref{fo:rules}) in
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