From a99d58a0f3957a16b90c781e14f8ad297dd35737 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Mon, 9 Oct 2023 17:15:35 -0400
Subject: [PATCH] formalism: Fix various typos in marked section

---
 formalism/marked.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/formalism/marked.tex b/formalism/marked.tex
index 3247289..ab49b24 100644
--- a/formalism/marked.tex
+++ b/formalism/marked.tex
@@ -130,7 +130,7 @@ \subsection{Unmarked expressions}
   }
 
   \inferrule[USLam]{
-    \ctxSynTypeU{\extendCtx{\ctx}{x}{\TMV}}{\EMV}{\TMV_2}
+    \ctxSynTypeU{\extendCtx{\ctx}{x}{\TMV_1}}{\EMV}{\TMV_2}
   }{
     \ctxSynTypeU{\ctx}{\ELam{x}{\TMV_1}{\EMV}}{\TArrow{\TMV_1}{\TMV_2}}
   }
@@ -388,7 +388,7 @@ \subsection{Marking}
     \ctxSynFixedInto{\ctx}{\EMV}{\ECMV}{\TMV} \\
     \notMatchedProd{\TMV}
   }{
-    \ctxSynFixedInto{\ctx}{\EProjL{\EMV}}{\ECProjLSynNonMatchedProd{\ECMV}}{\TMV_1}
+    \ctxSynFixedInto{\ctx}{\EProjL{\EMV}}{\ECProjLSynNonMatchedProd{\ECMV}}{\TUnknown}
   }
 
   \inferrule[MKSProjR1]{
@@ -402,7 +402,7 @@ \subsection{Marking}
     \ctxSynFixedInto{\ctx}{\EMV}{\ECMV}{\TMV} \\
     \notMatchedProd{\TMV}
   }{
-    \ctxSynFixedInto{\ctx}{\EProjR{\EMV}}{\ECProjRSynNonMatchedProd{\ECMV}}{\TMV_2}
+    \ctxSynFixedInto{\ctx}{\EProjR{\EMV}}{\ECProjRSynNonMatchedProd{\ECMV}}{\TUnknown}
   }
 \end{mathpar} \\
 
@@ -502,7 +502,7 @@ \subsection{Marked expressions}
   }
 
   \inferrule[MSLam]{
-    \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}
+    \ctxSynTypeM{\extendCtx{\ctx}{x}{\TMV_1}}{\ECMV}{\TMV_2}
   }{
     \ctxSynTypeM{\ctx}{\ECLam{x}{\TMV_1}{\ECMV}}{\TArrow{\TMV_1}{\TMV_2}}
   }