formalism: Move type meet in rules to premises

hazelgrove · Oct 9, 2023 · 7406abf · 7406abf
1 parent 116eb8c
commit 7406abf
Showing 1 changed file with 8 additions and 5 deletions.
diff --git a/formalism/marked.tex b/formalism/marked.tex
@@ -172,9 +172,10 @@ \subsection{Unmarked expressions}
   \inferrule[USIf]{
     \ctxAnaTypeU{\ctx}{\EMV_1}{\TBool} \\
     \ctxSynTypeU{\ctx}{\EMV_2}{\TMV_1} \\
-    \ctxSynTypeU{\ctx}{\EMV_3}{\TMV_2}
+    \ctxSynTypeU{\ctx}{\EMV_3}{\TMV_2} \\
+    \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
-    \ctxSynTypeU{\ctx}{\EIf{\EMV_1}{\EMV_2}{\EMV_3}}{\TMeet{\TMV_1}{\TMV_2}}
+    \ctxSynTypeU{\ctx}{\EIf{\EMV_1}{\EMV_2}{\EMV_3}}{\TMV_3}
   }
 
   \inferrule[USPair]{
@@ -354,9 +355,10 @@ \subsection{Marking}
   \inferrule[MKSIf]{
     \ctxAnaFixedInto{\ctx}{\EMV_1}{\ECMV_1}{\TBool} \\
     \ctxSynFixedInto{\ctx}{\EMV_2}{\ECMV_2}{\TMV_1} \\
-    \ctxSynFixedInto{\ctx}{\EMV_3}{\ECMV_3}{\TMV_2}
+    \ctxSynFixedInto{\ctx}{\EMV_3}{\ECMV_3}{\TMV_2} \\
+    \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
-    \ctxSynFixedInto{\ctx}{\EIf{\EMV_1}{\EMV_2}{\EMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMeet{\TMV_1}{\TMV_2}}
+    \ctxSynFixedInto{\ctx}{\EIf{\EMV_1}{\EMV_2}{\EMV_3}}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV_3}
   }
 
   \inferrule[MKSInconsistentBranches]{
@@ -551,8 +553,9 @@ \subsection{Marked expressions}
     \ctxAnaTypeM{\ctx}{\ECMV_1}{\TBool} \\
     \ctxSynTypeM{\ctx}{\ECMV_2}{\TMV_1} \\
     \ctxSynTypeM{\ctx}{\ECMV_3}{\TMV_2}
+    \TMV_3 = \TMeet{\TMV_1}{\TMV_2}
   }{
-    \ctxSynTypeM{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMeet{\TMV_1}{\TMV_2}}
+    \ctxSynTypeM{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV_3}
   }
 
   \inferrule[MSInconsistentBranches]{