formalism: Indicate domain/codomain for metafunctions

hazelgrove · Oct 10, 2023 · c70bb9d · c70bb9d
1 parent c03ab91
commit c70bb9d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/formalism/untyped.tex b/formalism/untyped.tex
@@ -36,7 +36,7 @@ \subsection{Cursor erasure}
 
 \subsubsection{Type cursor erasure}
 \label{sec:untyped-type-cursor-erasure}
-\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction $\ZTMName \to \TMName$ defined as follows:
 %
 \newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}}
 \[\begin{array}{rcl}
@@ -49,7 +49,7 @@ \subsubsection{Type cursor erasure}
 
 \subsubsection{Expression cursor erasure}
 \label{sec:untyped-expression-cursor-erasure}
-\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows:
+\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction $\ZMName \to \EMName$ defined as follows:
 %
 \[\begin{array}{rcl}
   \cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\