Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sum_type [2014/09/28 23:11]
nikolaj
sum_type [2015/10/07 16:50] (current)
nikolaj
Line 5: Line 5:
 | @#​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]]
Link to graph
Log In
Improvements of the human condition