From 184a0859806302c9b4e2925b67d503a35871b185 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Wed, 4 Oct 2023 16:12:11 -0400
Subject: [PATCH] formalism: Removed unmarked marking macros and rules

---
 formalism/marked.tex              | 32 -------------------------------
 formalism/symbols/expressions.tex |  2 --
 formalism/symbols/untyped.tex     |  2 --
 3 files changed, 36 deletions(-)

diff --git a/formalism/marked.tex b/formalism/marked.tex
index 24453ac..b95d4a1 100644
--- a/formalism/marked.tex
+++ b/formalism/marked.tex
@@ -317,22 +317,6 @@ \subsection{Marking}
     \ctxSynFixedInto{\ctx}{\EAp{\EMV_1}{\EMV_2}}{\ECAp{\ECMV_1}{\ECMV_2}}{\TMV_2}
   }
 
-  % \inferrule[MKSAp2]{
-    % \ctxSynFixedInto{\ctx}{\EMV_1}{\ECMV_1}{\TMV} \\
-    % \notMatchedArrow{\TMV} \\
-    % \ctxAnaFixedInto{\ctx}{\EMV_2}{\ECMV_2}{\TUnknown}
-  % }{
-    % \ctxSynFixedInto{\ctx}{\EAp{\EMV_1}{\EMV_2}}{\ECApNonMatched{\ECMV_1}{\ECMV_2}}{\TUnknown}
-  % }
-
-  % \inferrule[MKSAp2]{
-    % \ctxSynFixedInto{\ctx}{\EMV_1}{\ECMV_1}{\TMV} \\
-    % \notMatchedArrow{\TMV} \\
-    % \ctxAnaFixedInto{\ctx}{\EMV_2}{\ECMV_2}{\TUnknown}
-  % }{
-    % \ctxSynFixedInto{\ctx}{\EAp{\EMV_1}{\EMV_2}}{\ECApNonMatchedAlt{\ECMV_1}{\ECMV_2}}{\TUnknown}
-  % }
-
   \inferrule[MKSAp2]{
     \ctxSynFixedInto{\ctx}{\EMV_1}{\ECMV_1}{\TMV} \\
     \notMatchedArrow{\TMV} \\
@@ -529,22 +513,6 @@ \subsection{Marked expressions}
     \ctxSynTypeM{\ctx}{\ECAp{\ECMV_1}{\ECMV_2}}{\TMV_2}
   }
 
-  % \inferrule[MSAp2]{
-    % \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV} \\
-    % \notMatchedArrow{\TMV} \\
-    % \ctxAnaTypeM{\ctx}{\ECMV_2}{\TUnknown}
-  % }{
-    % \ctxSynTypeM{\ctx}{\ECApNonMatched{\ECMV_1}{\ECMV_2}}{\TUnknown}
-  % }
-
-  % \inferrule[MSAp2]{
-    % \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV} \\
-    % \notMatchedArrow{\TMV} \\
-    % \ctxAnaTypeM{\ctx}{\ECMV_2}{\TUnknown}
-  % }{
-    % \ctxSynTypeM{\ctx}{\ECApNonMatchedAlt{\ECMV}{\ECMV}}{\TUnknown}
-  % }
-
   \inferrule[MSAp2]{
     \ctxSynTypeM{\ctx}{\ECMV_1}{\TMV} \\
     \notMatchedArrow{\TMV} \\
diff --git a/formalism/symbols/expressions.tex b/formalism/symbols/expressions.tex
index 0d6b64b..7f907c5 100644
--- a/formalism/symbols/expressions.tex
+++ b/formalism/symbols/expressions.tex
@@ -58,8 +58,6 @@
 % lambdas
 \newcommand{\ECLam}[3]{\ensuremath{\lambda #1 : #2. ~#3}}
 \newcommand{\ECAp}[2]{\ensuremath{#1 ~#2}}
-\newcommand{\ECApNonMatched}[2]{\ensuremath{\ECAp{\ECInconType{#1}}{#2}}}
-\newcommand{\ECApNonMatchedAlt}[2]{\ensuremath{\textcolor{red}{[}\ECAp{#1}{#2}\textcolor{red}{]}}}
 
 % pairs
 \newcommand{\ECPair}[2]{\ensuremath{(#1, #2)}}
diff --git a/formalism/symbols/untyped.tex b/formalism/symbols/untyped.tex
index df8d9e4..f1e5c8f 100644
--- a/formalism/symbols/untyped.tex
+++ b/formalism/symbols/untyped.tex
@@ -37,8 +37,6 @@
 \newcommand{\ZLamE}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
 \newcommand{\ZApL}[2]{\ensuremath{\ECAp{#1}{#2}}}
 \newcommand{\ZApR}[2]{\ensuremath{\ECAp{#1}{#2}}}
-\newcommand{\ZApNonMatchedL}[2]{\ensuremath{\ECApNonMatched{#1}{#2}}}
-\newcommand{\ZApNonMatchedR}[2]{\ensuremath{\ECApNonMatched{#1}{#2}}}
 
 % booleans
 \newcommand{\ZIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}