Fix equational theory.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/lang.ltx b/sec/lang.ltx
index b26359f..e3fe075 100644
--- a/sec/lang.ltx
+++ b/sec/lang.ltx
@@ -200,13 +200,13 @@ such that \(\unroll~(\roll~t) = t\).
 
 \begin{figure}
   \begin{align*}
-    (\lambda x. t)~u &\coloneq \sub{t}{x/u}
+    (\lambda x. t)~u &= \sub{t}{x/u}
     &
-    \casetm{\tuple{k, t}}{\tuple{i,x_i}}{u_i}{i} &\coloneq \sub{u_k}{x_k/t}
+    \casetm{\hat{\ell}~t}{\ell~x_\ell}{u_\ell}{\ell} &= \sub{u_{\hat{\ell}}}{x_{\hat{\ell}}/t}
     \\
-    \tuple{\rangeover{t_i}{i}}.k &\coloneq t_k
+    \tuple{\rangeover{\ell : t_\ell}{\ell}}.\hat{\ell} &= t_{\hat{\ell}}
     &
-    \dofold{\roll~t}{x}{u} &\coloneq \sub{u}{x/\mapkw{}~(\lambda y. \dofold{y}{x}{u})~t}
+    \dofold{\roll~t}{x}{u} &= \sub{u}{x/\mapkw{}~(\lambda y. \dofold{y}{x}{u})~t}
   \end{align*}
   \caption{The equational theory of \lang{}}\label{fig:lang-theory}
 \end{figure}