===== Sum type =====
==== Type ====
| @#55CCEE:  context | @#55CCEE:  $X, Y, Z$ ... type |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{a\ :\ X}{\nu_{\mathcal l}(a)\ :\ X+Y}}(+\mathcal l \mathcal I)$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{b\ :\ Y}{\nu_{\mathcal r}(b)\ :\ X+Y}}(+\mathcal r \mathcal I)$ |
| @#FF8866:  rule | @#FF8866:  ${\large\frac{\Gamma,\ x\ :\ X\ \vdash\  f\ :\ Z\hspace{1cm}\Gamma,\ y\ :\ Y\ \vdash\  g\ :\ Z\hspace{1cm}c\ :\ X+Y}{\Gamma\ \vdash\ \left[\mathrm{\bf if}\,c\ \text{matches} \ \nu_{\mathcal l}(x)\ \text{do} \ f(x),\ \mathrm{\bf elseif}\, c\ \text{matches} \ \nu_{\mathcal r}(y)\ \text{do} \ g(y)\right]\ :\ Z}}(+\mathcal E)$ |

-----
=== Discussion ===
== Notation ==
The matching-term is generally written 

$\left[\nu_{\mathcal l}x.f(x),\ \nu_{\mathcal r}y.g(y)\right](c),$

which is shorter but less suggestive.

== Logic ==
Note how the rules reflect the logical "or".

-----
=== Element of ===
[[Type]]