formalism: Add mechanization indicator for constraint section

hazelgrove · Oct 10, 2023 · 5d37ee3 · 5d37ee3
1 parent 1b677e8
commit 5d37ee3
Showing 1 changed file with 2 additions and 0 deletions.
diff --git 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{ }{