formalism: Add missing markless rules

hazelgrove · Oct 9, 2023 · 5857aa3 · 5857aa3
1 parent ec5c9fe
commit 5857aa3
Showing 1 changed file with 26 additions and 0 deletions.
diff --git a/formalism/marked.tex b/formalism/marked.tex
@@ -758,6 +758,13 @@ \subsection{Marked expressions}
     \markless{\ECAp{\ECMV_1}{\ECMV_2}}
   }
 
+  \inferrule[MLLet]{
+    \markless{\ECMV_1} \\
+    \markless{\ECMV_2}
+  }{
+    \markless{\ECLet{x}{\ECMV_1}{\ECMV_2}}
+  }
+
   \inferrule[MLNum]{ }{
     \markless{\ECNumMV}
   }
@@ -784,6 +791,25 @@ \subsection{Marked expressions}
   }{
     \markless{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
+
+  \inferrule[MLPair]{
+    \markless{\ECMV_1} \\
+    \markless{\ECMV_2}
+  }{
+    \markless{\ECPair{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MLProjL]{
+    \markless{\ECMV} \\
+  }{
+    \markless{\ECProjL{\ECMV}}
+  }
+
+  \inferrule[MLProjR]{
+    \markless{\ECMV} \\
+  }{
+    \markless{\ECProjR{\ECMV}}
+  }
 \end{mathpar}
 
 \subsection{Mark erasure}