Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sum_type [2014/04/03 16:23] nikolaj |
sum_type [2015/10/07 16:50] nikolaj |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| | @#FF8866: rule | @#FF8866: ${\large\frac{a\ :\ X}{\nu_{\mathcal l}(a)\ :\ X+Y}}(+\mathcal l \mathcal I)$ | | | @#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{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)$ | | + | | @#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 ==== | + | |
| + | ----- | ||
| + | === Discussion === | ||
| == Notation == | == Notation == | ||
| The matching-term is generally written | The matching-term is generally written | ||
| Line 15: | Line 17: | ||
| == Logic == | == Logic == | ||
| Note how the rules reflect the logical "or". | Note how the rules reflect the logical "or". | ||
| - | ==== Parents ==== | + | |
| + | ----- | ||
| === Element of === | === Element of === | ||
| [[Type]] | [[Type]] | ||
