From 8c5d117581230548fc23110d2d6095762306adf7 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 29 Apr 2025 18:06:58 +0100
Subject: Fix pseudocode.

- Make `arb` a keyword.
- Correct argument order to `map`.
---
 sec/encoding.ltx | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'sec/encoding.ltx')

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 8de40c4..dc3f8c8 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -158,7 +158,7 @@ index of the given child.
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\), recursively encoding \(A\).
 We present the encoding of \roll*{} and \foldkw{} in
-\cref{fig:phase-2-encode}.
+\cref{fig:phase-2-encode}. 
 
 \TODO{
   \begin{itemize}
@@ -194,7 +194,7 @@ let compose (depth, heap) =
   let go = primrec depth with
     Zero   => arb
   | Suc ih => fun index =>
-    let x = map (heap index) (fun x => ih (snoc xs x)) in
+    let x = map (fun x => ih (snoc xs x)) (heap index) in
     match x with
       Leaf f        => f
     | Branch (f, g) => fun x => f (g x)
-- 
cgit v1.2.3