Improve multiline let formatting.

1 files changed, 9 insertions, 12 deletions

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.