Commit 21a3e35e authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent af47b1b9
......@@ -83,13 +83,12 @@ 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
subsumes $t$, $\apply t s$ is the smallest codomain of an arrow type
that subsumes $t$ and has domain $s$ and $\worra t s$ was explained
We need similar operators for projections since the type $t$
of $e$ in $\pi_i e$ may not be a single product type but, say, a union
of products: all we know is that $t$ must be a subtype of
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