formalism: Add polymorphic error forms to syntax description

hazelgrove · Jun 2, 2023 · fba8440 · fba8440
1 parent 600ddae
commit fba8440
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/formalism/polymorphism.tex b/formalism/polymorphism.tex
@@ -10,7 +10,8 @@ \subsubsection{Syntax}
                      % \mid \MTArrow{\MTMV}{\MTMV} \mid \MTProd{\MTMV}{\MTMV}
                      \mid \MTForall{\MTVarMV}{\MTMV} \mid \MTVarMV \mid \MTUnbound{\MTVarMV} \\
   \EMName  & \EMV  & \Coloneqq & \cdots \mid \ETypeLam{\TVarMV}{\EMV} \mid \ETypeAp{\EMV}{\TMV} \\
-  \ECMName & \ECMV & \Coloneqq & \cdots \mid \ECTypeLam{\MTVarMV}{\ECMV} \mid \ECTypeAp{\ECMV}{\MTMV}
+  \ECMName & \ECMV & \Coloneqq & \cdots \mid \ECTypeLam{\MTVarMV}{\ECMV} \mid \ECTypeAp{\ECMV}{\MTMV} \\
+           &       & \mid      & \ECSynNonMatchedForall{\ECMV} \mid \ECAnaNonMatchedForall{\ECMV}
 \end{array}\]
 
 \subsubsection{Unmarked types}