diff --git a/formalism/constraint.tex b/formalism/constraint.tex
new file mode 100644
index 0000000..8fb4d5b
--- /dev/null
+++ b/formalism/constraint.tex
@@ -0,0 +1,219 @@
+\documentclass[formalism.tex]{subfiles}
+
+\begin{document}
+\input{symbols/types}
+\input{symbols/expressions}
+\input{symbols/marked}
+\input{symbols/constraint}
+
+\section{Constraint generation}
+\label{constraint}
+
+A list of constraint generating bidirectional typing rules under the marked lambda calculus for type
+hole inference (see Section 4). \\
+
+\judgbox{\ensuremath{\matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched arrow type $\TArrow{\TMV_1}{\TMV_2}$ and generates constraints $C$
+\begin{mathpar}
+  \judgment{ }{
+    \matchedArrowConstraint{\TUnknown^p}{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}}{\{ \TUnknown^p \approx \tarr{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}} \}}
+  }{TMAHole-C}
+
+  \judgment{ }{
+    \matchedArrowConstraint{\TArrow{\TMV_1}{\TMV_2}}{\TMV_1}{\TMV_2}{\{\}}
+  }{TMAArr-C}
+\end{mathpar}
+
+\judgbox{\ensuremath{\matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched binary product type $\TProd{\TMV_1}{\TMV_2}$ and generates constraints $C$
+\begin{mathpar}
+  \judgment{ }{
+    \matchedProdConstraint{\TUnknown^p}{\TUnknown}{\TUnknown}{\{ \TUnknown^p \approx \TProd{\TUnknown^{\times_{L}(p)}}{\TUnknown^{\times_{R}(p)}} \}}
+  }{TMPHole-C}
+
+  \judgment{ }{
+    \matchedProdConstraint{\TProd{\TMV_1}{\TMV_2}}{\TMV_1}{\TMV_2}{\{\}}
+  }{TMPProd-C}
+\end{mathpar}
+
+\judgbox{\ensuremath{\synConstraint{\ctx}{\ECMV}{\TMV}{C}}} $\ECMV$ synthesizes type $\TMV$ and generates constraints $C$
+%
+\begin{mathparpagebreakable}
+  \judgment{ }{
+    \synConstraint{\ctx}{\EEHole^u}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSEHole-C}\\
+
+  \judgment{
+    \inCtx{\ctx}{x}{\TMV}
+  }{
+    \synConstraint{\ctx}{x}{\TMV}{\{\}}
+  }{MSVar-C}
+  
+  \judgment{
+    \notInCtx{\ctx}{x}
+  }{
+    \synConstraint{\ctx}{\ECFreeId{x}{u}}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSFree-C}
+
+  \judgment{
+    \synConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}{C}
+  }{
+    \synConstraint{\ctx}{\ECLam{x}{\TMV_1}{\ECMV}}{\TArrow{\TMV_1}{\TMV_2}}{C}
+  }{MSLam-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
+    \matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C_2} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_3}
+  }{
+    \synConstraint{\ctx}{\ECAp{\ECMV_1}{\ECMV_2}}{\TMV_2}{C_1 \cup C_2 \cup C_3}
+  }{MSAp1-C}
+
+    \judgment{
+    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
+    \notMatchedArrow{\TMV} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TUnknown^{\rightarrow_{L}(exp(u))}}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECApSynNonMatchedArrowId{\ECMV_1}{u}{\ECMV_2}}{\TUnknown^{\rightarrow_{R}(exp(u))}}{C_1 \cup C_2 \cup \{ \TUnknown^{exp(u)} \approx \tarr{\TUnknown^{\rightarrow_L(exp(u))}}{\TUnknown^{\rightarrow_R(exp(u))}}\}}
+  }{MSAp2-C}
+
+  \judgment{ }{
+      \synConstraint{\ctx}{\ECNumMV}{\TNum}{\{\}}
+  }{MSNum-C}
+
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TNum}{C_1}\\    \anaConstraint{\ctx}{\ECMV_2}{\TNum}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECPlus{\ECMV_1}{\ECMV_2}}{\TNum}{C_1 \cup C_2}
+  }{MSPlus-C}
+
+  \judgment{ }{
+    \synConstraint{\ctx}{\ECTrue}{\TBool}{\{\}}
+  }{MSTrue-C}
+
+  \judgment{ }{
+      \synConstraint{\ctx}{\ECFalse}{\TBool}{\{\}}
+  }{MSFalse-C}
+
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
+    \synConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_2} \\
+    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3}
+  }{
+    \synConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMeet{\TMV_1}{\TMV_2}}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2 \}}
+  }{MSIf-C}
+
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
+    \synConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_2} \\
+    \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3} \\
+    \inconsistent{\TMV_1}{\TMV_2}
+  }{
+    \synConstraint{\ctx}{\ECInconBrId{\ECMV_1}{\ECMV_2}{\ECMV_3}{u}}{\TUnknown^{exp(u)}}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2, \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSInconsistentBranches-C}
+  
+  \judgment{
+    \synConstraint{\ctx}{\ECMV_1}{\TMV_1}{C_1}\\
+    \synConstraint{\ctx}{\ECMV_2}{\TMV_2}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECPair{\ECMV_1}{\ECMV_2}}{\TProd{\TMV_1}{\TMV_2}}{C_1 \cup C_2}
+  }{MSPair-C}
+    
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV}{C_1} \\
+    \matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECProjL{\ECMV}}{\TMV_1}{C_1 \cup C_3}
+  }{MSProjL1-C}
+
+   \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV}{C_1} \\
+    \matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECProjR{\ECMV}}{\TMV_2}{C_1 \cup C_2}
+  }{MSProjR1-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV}{C} \\
+    \notMatchedProd{\TMV}
+  }{
+    \synConstraint{\ctx}{\ECProjL{\ECProjLSynNonMatchedProdId{\ECMV}{u}}}{\TUnknown^{\times_{L}(exp(u))}}{C \cup \{ \TUnknown^{exp(u)} \approx \TProd{\TUnknown^{\times_{L}(exp(u))}}{\TUnknown^{\times_{R}(exp(u))}}, \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSProjL2-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV}{C} \\
+    \notMatchedProd{\TMV}
+  }{
+    \synConstraint{\ctx}{\ECProjR{\ECProjRSynNonMatchedProdId{\ECMV}{u}}}{\TUnknown^{\times_{R}(exp(u))}}{C \cup \{ \TUnknown^{exp(u)} \approx \TProd{\TUnknown^{\times_{L}(exp(u))}}{\TUnknown^{\times_{R}(exp(u))}}, \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSProjR2-C}
+\end{mathparpagebreakable}
+
+\judgbox{\ensuremath{\anaConstraint{\ctx}{\ECMV}{\TMV}{C}}} $\ECMV$ analyzes against type $\TMV$ and generates constraints $C$
+%
+\begin{mathparpagebreakable}
+  \judgment{
+    \matchedArrowConstraint{\TMV_3}{\TMV_1}{\TMV_2}{C_1}\\
+    \consistent{\TMV}{\TMV_1} \\
+    \anaConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}{C_2}
+  }{
+    \anaConstraint{\ctx}{\ECLam{x}{\TMV}{\ECMV}}{\TMV_3}{C_1 \cup C_2 \cup \{ \TMV \approx \TMV_1 \}}
+  }{MALam1-C}
+
+  \judgment{
+    \notMatchedArrow{\TMV_3} \\
+    \anaConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TUnknown^{anon}}{C}
+  }{
+    \anaConstraint{\ctx}{\ECLamAnaNonMatchedArrowId{x}{\TMV}{\ECMV}{u}}{\TMV_3} {C \cup \{ \TUnknown^{exp(u)} \approx \TMV_3 \}}
+  }{MALam2-C}
+
+  \judgment{
+    \matchedArrowConstraint{\TMV_3}{\TMV_1}{\TMV_2}{C_1}\\
+    \inconsistent{\TMV}{\TMV_1} \\\\
+    \anaConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}{C_2}
+  }{
+    \anaConstraint{\ctx}{\ECInconTypeId{\ECLam{x}{\TMV}{\ECMV}}{u}}{\TMV_3} {C_1 \cup C_2 \cup \{ \TUnknown^{exp(u)} \approx \TMV_3 \}}
+  }{MALam3-C}
+
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
+    \anaConstraint{\ctx}{\ECMV_1}{\TMV}{C_2} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TMV}{C_3}
+  }{
+    \anaConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV}{C_1 \cup C_2 \cup C_3}
+  }{MAIf}  
+
+  \judgment{
+    \matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C_1} \\
+    \anaConstraint{\ctx}{\ECMV_1}{\TMV_1}{C_2} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TMV_2}{C_3}
+  }{
+    \anaConstraint{\ctx}{\ECPair{\ECMV_1}{\ECMV_2}}{\TMV}{C_1 \cup C_2 \cup C_3}
+  }{MAPair1-C}
+
+  \judgment{
+    \notMatchedProd{\TMV} \\
+    \anaConstraint{\ctx}{\ECMV_1}{\TUnknown^{anon}}{C_1} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TUnknown^{anon}}{C_2}
+  }{
+    \anaConstraint{\ctx}{
+      \ECPairAnaNonMatchedProdId{\ECMV_1}{\ECMV_2}{u}
+    }{\TMV}{C_1 \cup C_2 \cup \{\TUnknown^{exp(u)} \approx \tau\}}
+  }{MAPair2-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
+    \inconsistent{\TMV}{\TMV'} \\
+    \subsumable{\ECMV}
+  }{
+    \anaConstraint{\ctx}{\ECInconTypeId{\ECMV}{u}}{\TMV}{C \cup \{ \TMV \approx \TUnknown^{exp(u)} \}}
+  }{MAInconsistentTypes-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
+    \consistent{\TMV}{\TMV'} \\
+    \subsumable{\ECMV}
+  }{
+    \anaConstraint{\ctx}{\ECMV}{\TMV}{C \cup \{ \TMV \approx \TMV' \}}
+  }{MASubsume-C}
+\end{mathparpagebreakable}
+
+\end{document}
+
diff --git a/formalism/formalism.tex b/formalism/formalism.tex
index 0e2f57b..c135b44 100644
--- a/formalism/formalism.tex
+++ b/formalism/formalism.tex
@@ -25,5 +25,8 @@
 \newpage
 
 \subfile{typed}
+\newpage
+
+\subfile{constraint}
 
 \end{document}
diff --git a/formalism/preamble/utilities.tex b/formalism/preamble/utilities.tex
index 720a15f..48383ea 100644
--- a/formalism/preamble/utilities.tex
+++ b/formalism/preamble/utilities.tex
@@ -34,3 +34,4 @@
 %
 \DeclareMathOperator{\?}{?}
 \DeclareMathOperator{\dom}{dom}
+\DeclareMathOperator{\cod}{cod}
diff --git a/formalism/symbols/constraint.tex b/formalism/symbols/constraint.tex
new file mode 100644
index 0000000..c9d2c3a
--- /dev/null
+++ b/formalism/symbols/constraint.tex
@@ -0,0 +1,305 @@
+\newcommand{\judgment}[3]{\inferrule[#3]{#1}{#2}}
+
+%
+% provenances
+%
+\newcommand{\Prov}{{\normalfont\textsf{Provenance}}}
+\newcommand{\Provp}{\ensuremath{p}}
+
+% errors with id
+\newcommand{\ECMarkedId}[3]{\ensuremath{\textcolor{red}{\bm{\llparenthesis}}\textcolor{red}{#1}\textcolor{red}{\bm{\rrparenthesis}^{#3}_{#2}}}}
+\newcommand{\ECMarkedFreeId}[2]{\ensuremath{\ECMarkedId{#1}{\MRFree}{#2}}}
+\newcommand{\ECMarkedInconTypeId}[2]{\ensuremath{\ECMarkedId{#1}{\MRInconAsc}{#2}}}
+\newcommand{\ECMarkedInconBrId}[2]{\ensuremath{\ECMarkedId{#1}{\MRInconBr}{#2}}}
+
+\newcommand{\ECFreeId}[2]{\ensuremath{\ECMarkedFreeId{#1}{#2}}}
+\newcommand{\ECInconTypeId}[2]{\ensuremath{\ECMarkedInconTypeId{#1}{#2}}}
+\newcommand{\ECInconBrId}[4]{\ensuremath{\ECMarkedInconBrId{\ECIf{#1}{#2}{#3}}{#4}}}
+\newcommand{\ECApNonMatchedId}[3]{\ensuremath{\ECAp{\ECInconTypeId{#1}{#2}}{#3}}}
+
+\newcommand{\ECApSynNonMatchedArrowId}[3]{\ensuremath{\ECAp{\ECMarkedId{#1}{\MRSynNonMatchedArrow}{\MRSyn,~#2}}{#3}}}
+
+\newcommand{\ECLamAnaNonMatchedArrowId}[4]{\ECMarkedId{\ECLam{#1}{#2}{#3}}{\MRAnaNonMatchedArrow}{\MRAna,~#4}}
+
+\newcommand{\ECInconMatchedId}[3]{\ensuremath{\ECMarkedId{#1}{#2}{#3}}}
+\newcommand{\ECInconMatchedArrowId}[2]{\ensuremath{\ECInconMatchedId{#1}{\notMatchedArrowRel}{#2}}}
+\newcommand{\ECInconMatchedPairId}[2]{\ensuremath{\ECInconMatchedId{#1}{\notMatchedProdRel}{#2}}}
+
+\newcommand{\ECPairAnaNonMatchedProdId}[3]{\ECMarkedId{\ECPair{#1}{#2}}{\MRAnaNonMatchedProd}{\MRAna,~#3}}
+
+\newcommand{\ECProjLSynNonMatchedProdId}[2]{\ECMarkedId{#1}{\MRSynNonMatchedProd}{\MRSyn,~#2}}
+\newcommand{\ECProjRSynNonMatchedProdId}[2]{\ECMarkedId{#1}{\MRSynNonMatchedProd}{\MRSyn,~#2}}
+
+% Violet hotdogs; highlight color helps distinguish them
+\newcommand{\llparenthesiscolor}{\textcolor{violet}{\llparenthesis}}
+\newcommand{\rrparenthesiscolor}{\textcolor{violet}{\rrparenthesis}}
+
+% HTyp and HExp
+\newcommand{\hcomplete}[1]{#1~\mathsf{complete}}
+
+% HTyp
+\newcommand{\htau}{\dot{\tau}}
+
+\newcommand{\tarrnp}[2]{#1 \rightarrow #2}
+\newcommand{\trul}[2]{\inparens{#1 \Rightarrow #2}}
+\newcommand{\trulnp}[2]{#1 \Rightarrow #2}
+\newcommand{\tnum}{\mathtt{num}}
+\newcommand{\tbool}{\mathtt{bool}}
+\newcommand{\tehole}{\mathtt{?}}
+\newcommand{\tsum}[2]{\inparens{{#1} + {#2}}}
+\newcommand{\tprod}[2]{\inparens{{#1} \times {#2}}}
+\newcommand{\tunit}{\mathtt{1}}
+\newcommand{\tvoid}{\mathtt{0}}
+
+\newcommand{\tcompat}[2]{#1 \sim #2}
+\newcommand{\tincompat}[2]{#1 \nsim #2}
+
+% HExp
+\newcommand{\hexp}{\dot{e}}
+\newcommand{\hlam}[3]{\inparens{\lambda #1:#2.#3}}
+\newcommand{\hap}[2]{#1(#2)}
+\newcommand{\hapP}[2]{(#1)~(#2)} % Extra paren around function term
+\newcommand{\hnum}[1]{\underline{#1}}
+\newcommand{\hadd}[2]{\inparens{#1 + #2}}
+\newcommand{\hpair}[2]{\inparens{#1 , #2}}
+\newcommand{\htriv}{()}
+\newcommand{\hehole}[1]{\llparenthesiscolor\rrparenthesiscolor}
+\newcommand{\hhole}[2]{\llparenthesiscolor #1 \rrparenthesiscolor}
+\newcommand{\hindet}[1]{\lceil#1\rceil}
+\newcommand{\hinj}[2]{\mathtt{inj}_{#1}({#2})}
+\newcommand{\hinl}[2]{\mathtt{inl}_{#1}({#2})}
+\newcommand{\hinr}[2]{\mathtt{inr}_{#1}({#2})}
+\newcommand{\hinlp}[1]{\mathtt{inl}(#1)}
+\newcommand{\hinrp}[1]{\mathtt{inr}(#1)}
+\newcommand{\hmatch}[2]{\mathtt{match}(#1) \{#2\}}
+\newcommand{\hcase}[5]{\mathtt{case}({#1},{#2}.{#3},{#4}.{#5})}
+\newcommand{\hrules}[2]{#1 \mid #2}
+\newcommand{\hrulesP}[2]{\inparens{#1 \mid #2}}
+\newcommand{\hrul}[2]{#1 \Rightarrow #2}
+\newcommand{\hrulP}[2]{\inparens{#1 \Rightarrow #2}}
+
+\newcommand{\hGamma}{\dot{\Gamma}}
+\newcommand{\domof}[1]{\text{dom}(#1)}
+\newcommand{\hsyn}[3]{#1 \vdash #2 \Rightarrow #3}
+\newcommand{\hana}[3]{#1 \vdash #2 \Leftarrow #3}
+\newcommand{\hexptyp}[4]{#1 \mathbin{;} #2 \vdash #3 : #4}
+\newcommand{\hpattyp}[4]{#1 : #2 \dashV #3 \mathbin{;} #4}
+\newcommand{\hsubstyp}[2]{#1 : #2}
+\newcommand{\hpatmatch}[3]{#1 \vartriangleright #2 \dashV #3}
+\newcommand{\hnotmatch}[2]{#1 \mathbin{\bot} #2}
+\newcommand{\hmaymatch}[2]{#1 \mathbin{?} #2}
+\newcommand{\htrans}[2]{#1 \mapsto #2}
+
+\newcommand{\isVal}[1]{#1 ~\mathtt{val}}
+\newcommand{\isErr}[1]{#1 ~\mathtt{err}}
+\newcommand{\isIndet}[1]{#1 ~\mathtt{indet}}
+\newcommand{\isFinal}[1]{#1 ~\mathtt{final}}
+
+% ZTyp and ZExp
+\newcommand{\zlsel}[1]{{\bowtie}{#1}}
+\newcommand{\zrsel}[1]{{#1}{\bowtie}}
+\newcommand{\zwsel}[1]{
+  \setlength{\fboxsep}{0pt}
+  \colorbox{green!10!white!100}{
+    \ensuremath{{{\textcolor{Green}{{\hspace{-2px}\triangleright}}}}{#1}{\textcolor{Green}{\triangleleft{\vphantom{\tehole}}}}}}
+}
+
+\newcommand{\removeSel}[1]{#1^{\diamond}}
+
+% ZTyp
+\newcommand{\ztau}{\hat{\tau}}
+
+% ZExp
+\newcommand{\zexp}{\hat{e}}
+
+% Direction
+\newcommand{\dParent}{\mathtt{parent}}
+\newcommand{\dChildn}[1]{\mathtt{child}~\mathtt{{#1}}}
+\newcommand{\dChildnm}[1]{\mathtt{child}~{#1}}
+
+% Action
+\newcommand{\aMove}[1]{\mathtt{move}~#1}
+	\newcommand{\zrightmost}[1]{\mathsf{rightmost}(#1)}
+	\newcommand{\zleftmost}[1]{\mathsf{leftmost}(#1)}
+\newcommand{\aSelect}[1]{\mathtt{sel}~#1}
+\newcommand{\aDel}{\mathtt{del}}
+\newcommand{\aReplace}[1]{\mathtt{replace}~#1}
+\newcommand{\aConstruct}[1]{\mathtt{construct}~#1}
+\newcommand{\aConstructx}[1]{#1}
+\newcommand{\aFinish}{\mathtt{finish}}
+
+\newcommand{\performAna}[5]{#1 \vdash #2 \xlongrightarrow{#4} #5 \Leftarrow #3}
+\newcommand{\performAnaI}[5]{#1 \vdash #2 \xlongrightarrow{#4}\hspace{-3px}{}^{*}~ #5 \Leftarrow #3}
+\newcommand{\performSyn}[6]{#1 \vdash #2 \Rightarrow #3 \xlongrightarrow{#4} #5 \Rightarrow #6}
+\newcommand{\performSynI}[6]{#1 \vdash #2 \Rightarrow #3 \xlongrightarrow{#4}\hspace{-3px}{}^{*}~ #5 \Rightarrow #6}
+\newcommand{\performTyp}[3]{#1 \xlongrightarrow{#2} #3}
+\newcommand{\performTypI}[3]{#1 \xlongrightarrow{#2}\hspace{-3px}{}^{*}~#3}
+
+\newcommand{\performMove}[3]{#1 \xlongrightarrow{#2} #3}
+\newcommand{\performDel}[2]{#1 \xlongrightarrow{\aDel} #2}
+
+% Form
+\newcommand{\farr}{\mathtt{arrow}}
+\newcommand{\fnum}{\mathtt{num}}
+\newcommand{\fsum}{\mathtt{sum}}
+
+\newcommand{\fasc}{\mathtt{asc}}
+\newcommand{\fvar}[1]{\mathtt{var}~#1}
+\newcommand{\flam}[1]{\mathtt{lam}~#1}
+\newcommand{\fap}{\mathtt{ap}}
+% \newcommand{\farg}{\mathtt{arg}}
+\newcommand{\fnumlit}[1]{\mathtt{lit}~#1}
+\newcommand{\fplus}{\mathtt{plus}}
+\newcommand{\fhole}{\mathtt{hole}}
+\newcommand{\fnehole}{\mathtt{nehole}}
+
+\newcommand{\finj}[1]{\mathtt{inj}~#1}
+\newcommand{\fcase}[2]{\mathtt{case}~#1~#2}
+
+% Talk about formal rules in example
+\newcommand{\refrule}[1]{\textrm{Rule~(#1)}}
+
+\newcommand{\herase}[1]{\left|#1\right|_\textsf{erase}}
+
+\newcommand{\arrmatch}[2]{#1 \blacktriangleright_{\rightarrow} #2}
+
+
+\newcommand{\TABperformAna}[5]{#1 \vdash & #2                & \xlongrightarrow{#4} & #5 & \Leftarrow #3}
+\newcommand{\TABperformSyn}[6]{#1 \vdash & #2 \Rightarrow #3 & \xlongrightarrow{#4} & #5 \Rightarrow #6}
+\newcommand{\TABperformTyp}[3]{& #1 & \xlongrightarrow{#2} & #3}
+
+\newcommand{\TABperformMove}[3]{#1 & \xlongrightarrow{#2} & #3}
+\newcommand{\TABperformDel}[2]{#1 \xlongrightarrow{\aDel} #2}
+
+\newcommand{\sumhasmatched}[2]{#1 \mathrel{\textcolor{black}{\blacktriangleright_{+}}} #2}
+
+\newcommand{\subminsyn}[1]{\mathsf{submin}_{\Rightarrow}(#1)}
+\newcommand{\subminana}[1]{\mathsf{submin}_{\Leftarrow}(#1)}
+
+
+\newcommand{\inparens}[1]{{\color{gray}(}#1{\color{gray})}}
+
+%% rule names for appendix
+\newcommand{\rname}[1]{\textsc{#1}}
+\newcommand{\gap}{\vspace{7pt}}
+
+%% constraints
+\newcommand{\consexptyp}[4]{#1 \vdash #2 {\Rightarrow} #3 {~ \vert ~} #4}
+\newcommand{\ana}[4]{#1 \vdash #2 {\Leftarrow} #3 {~ \vert ~} #4}
+\newcommand{\consexptypnc}[3]{#1 \vdash #2 {\Rightarrow} #3}
+\newcommand{\ananc}[3]{#1 \vdash #2 {\Leftarrow} #3}
+\newcommand{\econs}{\{\}}
+\newcommand{\addcons}[1]{{~ \vert ~} #1}
+\newcommand{\typearrow}{\blacktriangleright_{\rightarrow}}
+\newcommand{\tarr}[2]{#1 \rightarrow #2}
+\newcommand{\lamfunc}[2]{( \lambda #1.#2 )}
+\newcommand{\ehole}{\llparenthesiscolor\rrparenthesiscolor}
+\newcommand{\notehole}[1]{\llparenthesiscolor #1 \rrparenthesiscolor}
+\newcommand{\underlinenum}[1]{\underline{#1}}
+\newcommand{\conless}[2]{#1 \sqsubseteq #2}
+
+\newcommand{\colorCText}{\colorUText}
+\newcommand{\colorCBkgSyn}{\colorUBkgSyn}
+\newcommand{\colorCBkgAna}{\colorUBkgAna}
+
+%
+% constraints
+%
+\newcommand{\constrain}[2]{{#1} \approx {#2}}
+\newcommand{\constraintCons}[2]{\normalfont\textsf{cons}(#1, #2)}
+\newcommand{\constraintNil}{[]}
+
+\newcommand{\matchedArrowConstraint}[4]{
+    \matchedArrow{#1}{#2}{#3}\goodcolor{\colorOkSideJudge}{~|~} {#4}
+}
+\newcommand{\matchedProdConstraint}[4]{
+    \matchedProd{#1}{#2}{#3}\goodcolor{\colorOkSideJudge}{~|~} {#4}
+}
+\newcommand{\constraintTurn}{\goodcolor{\colorCText}{\vdash}}
+\newcommand{\constraintBar}{\goodcolor{\colorCText}{~|~}}
+\newcommand{\constraintSyn}{\goodcolor{\colorCText}{\Rightarrow}}
+\newcommand{\constraintAna}{\goodcolor{\colorCText}{\Leftarrow}}
+\newcommand{\synConstraint}[4]{
+    \begin{highlightbox}{\colorCBkgSyn}
+    \ensuremath{{#1} \constraintTurn {#2} \constraintSyn {#3} \constraintBar {#4}}
+    \end{highlightbox}
+}
+\newcommand{\anaConstraint}[4]{
+    \begin{highlightbox}{\colorCBkgAna}
+    \ensuremath{{#1} \constraintTurn {#2} \constraintAna {#3} \constraintBar {#4}}
+    \end{highlightbox}
+}
+
+% type incomplete
+\newcommand{\incomplete}[1]{#1 ~ \normalfont\textsf{incomplete}}
+
+% potential type
+\newcommand{\PTUnknownVar}[1]{\ensuremath{#1}}
+\newcommand{\PTNum}{\ensuremath{{\normalfont\textsf{N}}}}
+\newcommand{\PTBool}{\ensuremath{{\normalfont\textsf{B}}}}
+\newcommand{\PTArrow}[2]{\ensuremath{#1 \to #2}}
+
+% potential types
+\newcommand{\ptypCons}[2]{\normalfont\textsf{cons}(#1, #2)}
+\newcommand{\ptypSingle}[1]{\normalfont\textsf{single}(#1)}
+
+% potential type set
+\newcommand{\ptsRep}[1]{\normalfont\textsf{rep}(#1)}
+\newcommand{\ptsLead}[1]{\normalfont\textsf{lead}(#1)}
+
+% PTGraph Elements and Membership
+\newcommand{\ptypGraphNode}[2]{#1\normalfont\textsf{ : }#2}
+\newcommand{\underGraph}[2]{#1~|~#2}
+\newcommand{\isIn}[2]{#1 \in #2}
+\newcommand{\isNotIn}[2]{#1 \notin #2}
+
+% PTGraph Update
+\newcommand{\ptypGraphUpdate}[4]{
+    \underGraph{#1}{\normalfont\textsf{update}~#2:#3 ~\hookrightarrow~ #4}
+}
+
+% PTGraph add node
+\newcommand{\ptypGraphAdd}[3]{
+    \underGraph{#1}{\normalfont\textsf{add}~#2 ~\hookrightarrow~ #3}
+}
+
+% PTSet Leader
+\newcommand{\leader}[4]{
+    \underGraph{#1}{\normalfont\textsf{leader}~#2 \equiv \ptypGraphNode{#3}{#4}}
+}
+
+% Unions
+\newcommand{\unionOf}[3]{#2 \cup_{#1} #3}
+
+%   Type Union
+\newcommand{\typUnion}[2]{\unionOf{\tau}{#1}{#2}}
+\newcommand{\ptypGraphUnion}[4]{
+    \underGraph{#1}{\typUnion{#2}{#3}} ~\hookrightarrow~ #4
+}
+
+% PTyps Union
+\newcommand{\ptypsUnion}[2]{#1~\Cup~#2}
+\newcommand{\specSubset}[3]{#1~\Subset_{#3}~#2}
+\newcommand{\ptypesSubset}[2]{\specSubset{#1}{#2}{u}}
+\newcommand{\ptypSetSubset}[3]{\underGraph{#1}{\specSubset{#2}{#3}{s}}}
+\newcommand{\snapSubset}[2]{\specSubset{#1}{#2}{j}}
+\newcommand{\snapElement}[2]{#1 ~\in_{h}~ #2}
+
+% unification
+\newcommand{\unify}[3]{\underGraph{#1}{#2~\amalg~#3}}
+
+% Snapshot PTS
+\newcommand{\ptsSnapshot}[3]{\underGraph{#1}{\normalfont\textsf{snapshot}_s~#2 \equiv #3}}
+
+% Snapshot List
+\newcommand{\listSnapshot}[3]{\underGraph{#1}{\normalfont\textsf{snapshot}_l~#2 \equiv #3}}
+
+% Solution
+\newcommand{\solution}[2]{\normalfont\textsf{solution}~#1 \equiv #2}
+
+% List
+\newcommand{\listCons}[2]{\normalfont\textsf{cons}(#1, #2)}
+\newcommand{\listNil}{\normalfont\textsf{nil}}
+
+% fresh
+\newcommand{\fresh}[1]{#1~\normalfont\textsf{fresh}}