diff options
| -rw-r--r-- | sec/lang.ltx | 8 |
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} |