mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-10-26 13:27:39 +03:00
typing: simplify the let rule
For some reason, it was written in a really complicated way that had no reason to be
This commit is contained in:
parent
25c754ccea
commit
06b84e27d7
@ -41,11 +41,10 @@
|
|||||||
\and
|
\and
|
||||||
\inferrule{%
|
\inferrule{%
|
||||||
\forall i \in \discrete{0}{n},
|
\forall i \in \discrete{0}{n},
|
||||||
\Gamma; x_i : \tau_{(1,i)}; \ldots; x_n: \tau_{(n,i)} \vdash e_i : \sigma_i \\
|
\Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e_i : \τ_i
|
||||||
\forall (i,j) \in \discrete{0}{n} \times \discrete{1}{n},
|
|
||||||
\sigma_j \subtype \tau_{(i,j)}
|
|
||||||
}{%
|
}{%
|
||||||
\Gamma \vdash \text{let } x_1 = e_1; \ldots{}; x_n = e_n \text{ in } e_0 : \sigma_0
|
\Gamma \vdash \text{let } x_1 : \τ_1 = e_1; \ldots{}; x_n : \τ_n = e_n
|
||||||
|
\text{ in } e_0 : \τ_0
|
||||||
}
|
}
|
||||||
(Let)
|
(Let)
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
|
Loading…
Reference in New Issue
Block a user