formalism: Unify ordering of rules and definitions

hazelgrove · Jul 11, 2023 · 9312d4b · 9312d4b
1 parent 214eeda
commit 9312d4b
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/formalism/marked.tex b/formalism/marked.tex
@@ -825,26 +825,26 @@ \subsection{Mark erasure}
 \[\begin{array}{rcl}
   \erasesToRow{\ECEHole}{\EEHole} \\
   \erasesToRow{x}{x} \\
+  \erasesToRow{\ECUnbound{x}}{x} \\
   \erasesToRow{(\ECLam{x}{\TMV}{\ECMV})}{\ELam{x}{\TMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ELam{x}{\TMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ECLam{x}{\TMV}{(\erase{\ECMV})}} \\
   \erasesToRow{(\ECAp{\ECMV_1}{\ECMV_2})}{\EAp{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
+  \erasesToRow{(\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2})}{\ECAp{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
   \erasesToRow{(\ECLet{x}{\ECMV_1}{\ECMV_2})}{\ELet{x}{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
   \erasesToRow{\ECNumMV}{\ENumMV} \\
   \erasesToRow{(\ECPlus{\ECMV_1}{\ECMV_2})}{\EPlus{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
   \erasesToRow{\ECTrue}{\ETrue} \\
   \erasesToRow{\ECFalse}{\EFalse} \\
   \erasesToRow{(\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3})}{\EIf{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ECMV_3})}} \\
+  \erasesToRow{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\EIf{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ECMV_3})}} \\
   \erasesToRow{\ECPair{\ECMV_1}{\ECMV_2}}{\ECPair{\erase{\ECMV_1}}{\erase{\ECMV_2}}} \\
+  \erasesToRow{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ECPair{\erase{\ECMV_1}}{\erase{\ECMV_2}}} \\
   \erasesToRow{(\ECProjL{\ECMV})}{\ECProjL{(\erase{\ECMV})}} \\
-  \erasesToRow{(\ECProjR{\ECMV})}{\ECProjR{(\erase{\ECMV})}} \\
-  \erasesToRow{\ECUnbound{x}}{x} \\
-  \erasesToRow{\ECInconType{\ECMV}}{\erase{\ECMV}} \\
-  \erasesToRow{\ECInconBr{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\EIf{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}{(\erase{\ECMV_3})}} \\
-  \erasesToRow{\ECLamInconAsc{x}{\TMV}{\ECMV}}{\ELam{x}{\TMV}{(\erase{\ECMV})}} \\
-  \erasesToRow{(\ECApSynNonMatchedArrow{\ECMV_1}{\ECMV_2})}{\ECAp{(\erase{\ECMV_1})}{(\erase{\ECMV_2})}} \\
   \erasesToRow{(\ECProjLSynNonMatchedProd{\ECMV})}{\ECProjL{(\erase{\ECMV})}} \\
+  \erasesToRow{(\ECProjR{\ECMV})}{\ECProjR{(\erase{\ECMV})}} \\
   \erasesToRow{(\ECProjRSynNonMatchedProd{\ECMV})}{\ECProjR{(\erase{\ECMV})}} \\
-  \erasesToRow{\ECLamAnaNonMatchedArrow{x}{\TMV}{\ECMV}}{\ECLam{x}{\TMV}{(\erase{\ECMV})}} \\
-  \erasesToRow{\ECPairAnaNonMatchedProd{\ECMV_1}{\ECMV_2}}{\ECPair{\erase{\ECMV_1}}{\erase{\ECMV_2}}} \\
+  \erasesToRow{\ECInconType{\ECMV}}{\erase{\ECMV}} \\
 \end{array}\]
 
 \subsection{Metatheorems}

diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -548,9 +548,9 @@ \subsection{Mark erasure}
 \[\begin{array}{rcl}
   & \vdots & \\
   \erasesToRow{(\ECTypeLam{\MTVarMV}{\ECMV})}{\ETypeLam{\MTVarMV}{(\erase{\ECMV})}} \\
+  \erasesToRow{\ECTypeLamAnaNonMatchedForall{\MTVarMV}{\ECMV}}{\ETypeLam{\MTVarMV}{(\erase{\ECMV})}} \\
   \erasesToRow{(\ECTypeAp{\ECMV}{\MTMV})}{\ETypeAp{\erase{\ECMV}}{\erase{\MTMV}}} \\
   \erasesToRow{(\ECTypeApSynNonMatchedForall{\ECMV}{\MTMV})}{\ETypeAp{\erase{\ECMV}}{\erase{\MTMV}}} \\
-  \erasesToRow{\ECTypeLamAnaNonMatchedForall{\MTVarMV}{\ECMV}}{\ETypeLam{\MTVarMV}{(\erase{\ECMV})}} \\
 \end{array}\]
 
 \subsection{Metatheorems}