Go backward to Product Go up to Top Go forward to Functions |
Concept of disjoint union
{ (zero,x) | x in R } union{ (one,y) | y in S }
"tags" to preserve origin of element
inR(x) = (zero, x) (for x in R)
inS(x) = (one, y) (for y in S)
cases m of
isR(x) => ...x ... isS(y) => ...y ... end
m=(zero,x) => ...x ...
m=(zero,y) => ...y ...