Types somme I
Union disjointe d'ensembles:
t = A Å B = {x.g | x Î A} È {y.d | y Î B}
Injection canonique
-
gauche : A ® A Å B
-
droit : A ® A Å B
On a x:t ssi
$ y1:t1 tq x = g(y1) XOR
$ y2:t2 tq x = d(y2)
En Caml, ces injection sont données par l'utilisateur au moment de
la définition du type.