# Differences

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

 sum_type [2014/09/28 23:11]nikolaj sum_type [2015/10/07 16:50] (current)nikolaj Both sides previous revision Previous revision 2015/10/07 16:50 nikolaj 2014/09/28 23:11 nikolaj 2014/04/03 16:23 nikolaj 2014/04/01 14:13 nikolaj 2014/03/30 20:09 nikolaj 2014/03/30 20:09 nikolaj 2014/03/30 19:44 nikolaj 2014/03/30 19:43 nikolaj 2014/03/30 19:43 nikolaj 2014/03/30 18:50 nikolaj old revision restored (2014/03/30 17:53) 2015/10/07 16:50 nikolaj 2014/09/28 23:11 nikolaj 2014/04/03 16:23 nikolaj 2014/04/01 14:13 nikolaj 2014/03/30 20:09 nikolaj 2014/03/30 20:09 nikolaj 2014/03/30 19:44 nikolaj 2014/03/30 19:43 nikolaj 2014/03/30 19:43 nikolaj 2014/03/30 18:50 nikolaj old revision restored (2014/03/30 17:53) 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]]