typing: add typing rule for merge

This commit is contained in:
regnat 2017-04-06 09:00:14 +02:00
parent ff04f8828f
commit bcf70bac37

View File

@ -231,6 +231,14 @@ n\right\}$, $l_i = k_{\σ(i)}$ and $v_i \subtype w_{\σ(i)}$.
}{%
\vdash e_1 \orthplus e_2 : \tau \orthplus \sigma
}
\and
\inferrule{%
\vdash e_1 : \tau \\ \vdash e_2 : \σ \\
\tau \subtype \onerec{} \\
\sigma \subtype \onerec{}
}{%
\vdash e_1 + e_2 : \tau + \sigma
}
\end{mathpar}
\bibliographystyle{alpha}