From 4ae30cf7efb8358220510dc46a17e7ba99747d58 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 25 Jun 2025 17:22:18 +0100
Subject: Fix equational theory.

---
 sec/lang.ltx | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'sec/lang.ltx')

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}
-- 
cgit v1.2.3

