formalism: Replace "markless" judgement(s) with "marked" judgment(s)

formalism/marked.tex

@@ -752,55 +752,127 @@ \subsection{Marked expressions}
   }
 \end{mathpar} \\
 
-\judgbox{\markless{\ECMV}} $\ECMV$ has no marks
+\judgbox{\marked{\ECMV}} $\ECMV$ has some mark
 %
 \begin{mathpar}
-  \inferrule[MLHole]{ }{
-    \markless{\ECEHole}
+  \inferrule[MDUnbound]{ }{
+    \marked{\ECUnbound{x}}
   }
 
-  \inferrule[MLVar]{ }{
-    \markless{x}
+  \inferrule[MDLam1]{
+    \marked{\ECMV}
+  }{
+    \marked{\ECLam{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[MDLam2]{ }{
+    \marked{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[MDLam3]{ }{
+    \marked{\ECLamInconAsc{x}{\TMV}{\ECMV}}
+  }
+
+  \inferrule[MDAp1]{
+    \marked{\ECMV_1}
+  }{
+    \marked{\ECAp{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDAp2]{
+    \marked{\ECMV_2}
+  }{
+    \marked{\ECAp{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDAp3]{ }{
+    \marked{\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDLet1]{
+    \marked{\ECMV_1}
+  }{
+    \marked{\ECLet{x}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDLet2]{
+    \marked{\ECMV_2}
+  }{
+    \marked{\ECLet{x}{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLLam]{
-    \markless{\ECMV}
+  \inferrule[MDPlus1]{
+    \marked{\ECMV_1}
   }{
-    \markless{\ECLam{x}{\TMV}{\ECMV}}
+    \marked{\ECPlus{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLAp]{
-    \markless{\ECMV_1} \\
-    \markless{\ECMV_2}
+  \inferrule[MDPlus2]{
+    \marked{\ECMV_2}
   }{
-    \markless{\ECAp{\ECMV_1}{\ECMV_2}}
+    \marked{\ECPlus{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLNum]{ }{
-    \markless{\ECNumMV}
+  \inferrule[MDIf1]{
+    \marked{\ECMV_1}
+  }{
+    \marked{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+  }
+
+  \inferrule[MDIf2]{
+    \marked{\ECMV_2}
+  }{
+    \marked{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+  }
+
+  \inferrule[MDIf3]{
+    \marked{\ECMV_3}
+  }{
+    \marked{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
   }
 
-  \inferrule[MLPlus]{
-    \markless{\ECMV_1} \\
-    \markless{\ECMV_2}
+  \inferrule[MDInconsistentBranches]{ }{
+    \marked{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+  }
+
+  \inferrule[MDPair1]{
+    \marked{\ECMV_1}
   }{
-    \markless{\ECPlus{\ECMV_1}{\ECMV_2}}
+    \marked{\ECPair{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLTrue]{ }{
-    \markless{\ECTrue}
+  \inferrule[MDPair2]{
+    \marked{\ECMV_2}
+  }{
+    \marked{\ECPair{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLFalse]{ }{
-    \markless{\ECFalse}
+  \inferrule[MDPair3]{ }{
+    \marked{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}
   }
 
-  \inferrule[MLIf]{
-    \markless{\ECMV_1} \\
-    \markless{\ECMV_2} \\
-    \markless{\ECMV_3}
+  \inferrule[MDProjL1]{
+    \marked{\ECMV}
   }{
-    \markless{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}
+    \marked{\ECProjL{\ECMV}}
+  }
+
+  \inferrule[MDProjL2]{ }{
+    \marked{\ECProjLSynNonMatchedProd{\ECMV}}
+  }
+
+  \inferrule[MDProjR1]{
+    \marked{\ECMV}
+  }{
+    \marked{\ECProjR{\ECMV}}
+  }
+
+  \inferrule[MDProjR2]{ }{
+    \marked{\ECProjRSynNonMatchedProd{\ECMV}}
+  }
+
+  \inferrule[MDInconsistentTypes]{ }{
+    \marked{\ECInconType{\ECMV}}
   }
 \end{mathpar}
 
@@ -854,18 +926,18 @@ \subsection{Metatheorems}
   \begin{enumerate}
     \item \begin{enumerate}
         \item If $\ctxSynTypeU{\ctx}{\EMV}{\TMV}$ and $\ctxSynFixedInto{\ctx}{\EMV}{\ECMV}{\TMV}$,
-          then $\markless{\ECMV}$.
+          then it is not the case that $\marked{\ECMV}$.
         \item If $\ctxAnaTypeU{\ctx}{\EMV}{\TMV}$ and $\ctxAnaFixedInto{\ctx}{\EMV}{\ECMV}{\TMV}$,
-          then $\markless{\ECMV}$.
+          then it is not the case that $\marked{\ECMV}$.
       \end{enumerate}
 
     \item \begin{enumerate}
         \item If there does not exist $\TMV$ such that $\ctxSynTypeU{\ctx}{\EMV}{\TMV}$, then for
-          all $\ECMV$ and $\TMV'$ such that $\ctxSynFixedInto{\ctx}{\EMV}{\ECMV}{\TMV'}$, it is not
-          the case that $\markless{\ECMV}$.
+          all $\ECMV$ and $\TMV'$ such that $\ctxSynFixedInto{\ctx}{\EMV}{\ECMV}{\TMV'}$, it is the
+          case that $\marked{\ECMV}$.
         \item If there does not exist $\TMV$ such that $\ctxAnaTypeU{\ctx}{\EMV}{\TMV}$, then for
-          all $\ECMV$ and $\TMV'$ such that $\ctxAnaFixedInto{\ctx}{\EMV}{\ECMV}{\TMV'}$, it is not
-          the case that $\markless{\ECMV}$.
+          all $\ECMV$ and $\TMV'$ such that $\ctxAnaFixedInto{\ctx}{\EMV}{\ECMV}{\TMV'}$, it is the
+          case that $\marked{\ECMV}$.
       \end{enumerate}
   \end{enumerate}
 \end{theorem}

formalism/patterned.tex

@@ -171,15 +171,25 @@ \subsection{Marked expressions}
   }
 \end{mathpar}
 
-\judgbox{\markless{\ECMV}} $\ECMV$ has no marks
+\judgbox{\marked{\ECMV}} $\ECMV$ has some mark
 %
 \begin{mathpar}
-  \inferrule[MLLetPat]{
-    \markless{\PCMV} \\
-    \markless{\ECMV_1} \\
-    \markless{\ECMV_2}
+  \inferrule[MDLetPat1]{
+    \marked{\PCMV}
   }{
-    \markless{\ECLet{\PCMV}{\ECMV_1}{\ECMV_2}}
+    \marked{\ECLet{\PCMV}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDLetPat2]{
+    \marked{\ECMV_1}
+  }{
+    \marked{\ECLet{\PCMV}{\ECMV_1}{\ECMV_2}}
+  }
+
+  \inferrule[MDLetPat3]{
+    \marked{\ECMV_2}
+  }{
+    \marked{\ECLet{\PCMV}{\ECMV_1}{\ECMV_2}}
   }
 \end{mathpar}
 
@@ -393,28 +403,35 @@ \subsection{Marked patterns}
   }
 \end{mathpar}
 
-\judgbox{\markless{\PCMV}} $\PCMV$ has no marks
+\judgbox{\marked{\PCMV}} $\PCMV$ has some mark
 %
 \begin{mathpar}
-  \inferrule[MLPWild]{ }{
-    \markless{\PCWild}
+  \inferrule[MDPPair1]{
+    \marked{\PCMV_1}
+  }{
+    \marked{\PCPair{\PCMV_1}{\PCMV_2}}
+  }
+
+  \inferrule[MDPPair2]{
+    \marked{\PCMV_2}
+  }{
+    \marked{\PCPair{\PCMV_1}{\PCMV_2}}
   }
 
-  \inferrule[MLPVar]{ }{
-    \markless{\PCVar{x}}
+  \inferrule[MDPPair3]{ }{
+    \marked{\PCAnaNonMatchedProd{\PCPair{\PCMV_1}{\PCMV_2}}}
   }
 
-  \inferrule[MLPPair]{
-    \markless{\PCMV_1} \\
-    \markless{\PCMV_2}
+  \inferrule[MDPAnn1]{
+    \marked{\PCMV}
   }{
-    \markless{\PCPair{\PCMV_1}{\PCMV_2}}
+    \marked{\PCAsc{\PCMV}{\TMV}}
   }
 
-  \inferrule[MLPAnn]{
-    \markless{\PCMV}
+  \inferrule[MDPAnn2]{
+    \marked{\PCMV}
   }{
-    \markless{\PCAsc{\PCMV}{\TMV}}
+    \marked{\PCInconType{\PCAsc{\PCMV}{\TMV}}}
   }
 \end{mathpar}
 
@@ -466,24 +483,24 @@ \subsection{Metatheorems}
     \item \begin{enumerate}
         \item If $\ctxSynPatU{\ctx}{\PMV}{\TMV}$
             and $\ctxSynFixedIntoPat{\ctx}{\PMV}{\PCMV}{\TMV}$,
-          then $\markless{\PCMV}$.
+          then it is not the case that $\marked{\PCMV}$.
 
         \item If $\ctxAnaPatU{\ctx}{\PMV}{\TMV}{\ctx'}$
             and $\ctxAnaFixedIntoPat{\ctx}{\PMV}{\PCMV}{\TMV}{\ctx'}$,
-          then $\markless{\PCMV}$.
+          then it is not the case that $\marked{\PCMV}$.
       \end{enumerate}
 
     \item \begin{enumerate}
         \item If there does not exist $\TMV$
             such that $\ctxSynPatU{\ctx}{\PMV}{\TMV}$,
           then for all $\PCMV$ and $\TMV'$
             such that $\ctxSynFixedIntoPat{\ctx}{\PMV}{\PCMV}{\TMV'}$,
-            it is not the case that $\markless{\PCMV}$.
+            it is the case that $\marked{\PCMV}$.
 
         \item If there does not exist $\TMV$ and $\ctx'$ such that $\ctxAnaPatU{\ctx}{\PMV}{\TMV}{\ctx'}$,
           then for all $\PCMV$, $\TMV'$, and $\ctx'$
             such that $\ctxAnaFixedIntoPat{\ctx}{\PMV}{\PCMV}{\TMV'}{\ctx'}$,
-            it is not the case that $\markless{\PCMV}$.
+            it is the case that $\marked{\PCMV}$.
       \end{enumerate}
   \end{enumerate}
 \end{theorem}

formalism/symbols/marked.tex

@@ -74,8 +74,8 @@
 % subsumable
 \newcommand{\subsumable}[1]{\ensuremath{#1 ~{\normalfont\textsf{subsumable}}}}
 
-% markless
-\newcommand{\markless}[1]{\ensuremath{#1 ~{\normalfont\textsf{markless}}}}
+% marked
+\newcommand{\marked}[1]{\ensuremath{#1 ~{\normalfont\textsf{marked}}}}
 
 % mark erasure
 \newcommand{\erase}[1]{\ensuremath{#1^{\square}}}