From 6385ecf96cd60885c221e3144b5a5ec63eb5c831 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 Jun 2023 17:57:48 +0100
Subject: Add encodings for containers.

Remove useless junk.
---
 src/Encoded/Arith.idr | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

(limited to 'src/Encoded/Arith.idr')

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
index d2f83bc..fe9bc68 100644
--- a/src/Encoded/Arith.idr
+++ b/src/Encoded/Arith.idr
@@ -32,10 +32,15 @@ pred = Abs'
   (\n => App
     (Rec n
       (Const Zero)
-      (Abs' (\f =>
-        Rec (App f [<Zero])
-          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
-          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+      (Abs $ Abs $
+        let f = Var (There Here) in
+        let k = Var Here in
+        Rec k
+          (Lit 1)
+          (Const $
+            Rec (App f [<Zero])
+              Zero
+              (Const $ Suc $ App f [<Lit 1]))))
     [<Lit 1])
 
 export
@@ -76,6 +81,6 @@ divmod = Abs $ Abs $
     (App pair [<Zero, Zero])
     (Abs' (\p =>
       App if'
-        [<App lte [<shift d, App snd [<p]]
+        [<App lte [<shift d, Suc (App snd [<p])]
         , App pair [<Suc (App fst [<p]), Zero]
         , App mapSnd [<Abs' Suc, p]]))
-- 
cgit v1.2.3