formalism: Move type meet out of premise in MSIf-C

hazelgrove · Oct 27, 2023 · a529976 · a529976
1 parent 2dd1f15
commit a529976
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/formalism/constraint.tex b/formalism/constraint.tex
@@ -97,9 +97,10 @@ \section{Constraint generation}
   \judgment{
     \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
     \synConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_2} \\
-    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3}
+    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3} \\
+    \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
-    \synConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMeet{\TMV_1}{\TMV_2}}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2 \}}
+    \synConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV_3}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2 \}}
   }{MSIf-C}
 
   \judgment{