From 5d37ee31a7f08b6cbcaaa4ef69d23cbfd8268987 Mon Sep 17 00:00:00 2001
From: Eric Zhao <21zhaoe@protonmail.com>
Date: Tue, 10 Oct 2023 03:23:31 -0400
Subject: [PATCH] formalism: Add mechanization indicator for constraint section

---
 formalism/constraint.tex | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/formalism/constraint.tex b/formalism/constraint.tex
index 0a0d887..a0245dd 100644
--- a/formalism/constraint.tex
+++ b/formalism/constraint.tex
@@ -11,6 +11,8 @@ \section{Constraint generation}
 Here, we give the list of constraint-generating bidirectional typing rules under the marked lambda
 calculus for type hole inference, described in Section 4 of the paper.
 
+\nomechanization{}
+
 \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{ }{