From 4ae30cf7efb8358220510dc46a17e7ba99747d58 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 25 Jun 2025 17:22:18 +0100 Subject: Fix equational theory. --- sec/lang.ltx | 8 ++++---- 1 file 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} -- cgit v1.2.3