From 4459595f44adb15a1e88e63ee7e97e574fbb3a79 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 23 Apr 2025 16:37:39 +0100
Subject: Improve multiline let formatting.

---
 sec/systemt.ltx | 21 +++++++++------------
 1 file changed, 9 insertions(+), 12 deletions(-)

(limited to 'sec/systemt.ltx')

diff --git a/sec/systemt.ltx b/sec/systemt.ltx
index 54ba5f2..e66f499 100644
--- a/sec/systemt.ltx
+++ b/sec/systemt.ltx
@@ -171,8 +171,8 @@ the fold. Below is the fold over binary trees.
     \mathsf{leaf}(n). f(n);
     \mathsf{branch}(x, y). g(x, y)
   } \coloneq
-  \dolet{
-    go = \doprimrec*{t}{\arb}{h}{
+  \dolet{go}*{
+    \doprimrec*{t}{\arb}{h}{
       \lambda i. \domatch*{i}{
         \mathsf{leaf}(n). f(n);
         \mathsf{branch}(l, r). g(h(l), h(r))}}
@@ -206,21 +206,18 @@ respectively, and then case split on this sum. We detail this in \cref{fig:churc
       \mathsf{leaf}(n).     f(n);
       \mathsf{branch}(x,y). g(x, y)
     } \coloneq
-    \dolet[t]{
-      \roll = \lambda x. \domatch*[t]{x}{
+    \dolet[t]{\roll}*{
+      \lambda x. \domatch*[t]{x}{
         \mathsf{Left}(n).     \mathsf{leaf}(n);
-        \mathsf{Right}(x, y). \mathsf{branch}(x, y)
-      }
-    }{
-      x = \dofoldmatch*{t}{
+        \mathsf{Right}(x, y). \mathsf{branch}(x, y)}
+    }{x}*{
+      \dofoldmatch*{t}{
         \mathsf{leaf}(n).      \mathsf{Left}(n);
-        \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y)
-      }
+        \mathsf{branch}(x, y). \mathsf{Right}(\roll~x, \roll~y)}
     }*{
       \domatch*{x}{
         \mathsf{Left}(n).     f(n);
-        \mathsf{Right}(x, y). g(x, y)
-      }
+        \mathsf{Right}(x, y). g(x, y)}
     }
   \]
   \caption{How to perform pattern matching on binary trees for Church encodings.
-- 
cgit v1.2.3

