From 06b84e27d71d68f829353e2b11d235e4bfd45f48 Mon Sep 17 00:00:00 2001
From: regnat <rg@regnat.ovh>
Date: Fri, 21 Apr 2017 15:25:13 +0200
Subject: [PATCH] typing: simplify the let rule

For some reason, it was written in a really complicated way that had no
reason to be
---
 typing/type-system.tex | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/typing/type-system.tex b/typing/type-system.tex
index 6b0cfae..5c67cc6 100644
--- a/typing/type-system.tex
+++ b/typing/type-system.tex
@@ -41,11 +41,10 @@
   \and
   \inferrule{%
     \forall i \in \discrete{0}{n},
-      \Gamma; x_i : \tau_{(1,i)}; \ldots; x_n: \tau_{(n,i)} \vdash e_i : \sigma_i \\
-    \forall (i,j) \in \discrete{0}{n} \times \discrete{1}{n},
-      \sigma_j \subtype \tau_{(i,j)}
+      \Γ; x_1 : \τ_1; \ldots; x_n : \τ_n \vdash e_i : \τ_i
   }{%
-    \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)
 \end{mathpar}