mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-09-11 13:00:34 +03:00
typing: remove typing rules for static labels
They are included in the one for dynamic labels anyway
This commit is contained in:
parent
6c0a079eb4
commit
18fd26fc33
@ -202,22 +202,6 @@ of $\left\{1, \ldots{}, n\right\}$ such that for all $i \in \left\{1, \ldots{},
|
||||
n\right\}$, $l_i = k_{\σ(i)}$ and $v_i \subtype w_{\σ(i)}$.
|
||||
|
||||
\subsection{Typing rules}
|
||||
\subsubsection{Static labels}
|
||||
\begin{mathpar}
|
||||
\inferrule{%
|
||||
\Γ \vdash e : \τ
|
||||
}{%
|
||||
\Γ \vdash \{ l = e \} : \{ l: \τ \}
|
||||
}
|
||||
\and
|
||||
\inferrule{%
|
||||
\Γ \vdash e_1 : \τ \\ \Γ \vdash e_2 : \sigma \\%
|
||||
\dom_\undef(\tau) \wedge \dom_\undef(\sigma) = \varnothing
|
||||
}{%
|
||||
\Γ \vdash e_1 \orthplus e_2 : \tau \orthplus \sigma
|
||||
}
|
||||
\end{mathpar}
|
||||
|
||||
\subsubsection{Dynamic labels}
|
||||
\begin{mathpar}
|
||||
\inferrule{%
|
||||
|
Loading…
Reference in New Issue
Block a user