Add more built-in functions.

1 files changed, 1 insertions, 54 deletions

diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
index fe9bc68..4dd3e10 100644
--- a/src/Encoded/Arith.idr
+++ b/src/Encoded/Arith.idr
@@ -22,47 +22,8 @@ rec = Abs $ Abs $ Abs $
   App snd [<p]
 
 export
-plus : Term (N ~> N ~> N) ctx
-plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
-
-export
-pred : Term (N ~> N) ctx
--- pred = Abs' (\n => App rec [<n, Zero, fst])
-pred = Abs'
-  (\n => App
-    (Rec n
-      (Const Zero)
-      (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
-minus : Term (N ~> N ~> N) ctx
-minus = Abs $ Abs $
-  let m = Var $ There Here in
-  let n = Var Here in
-  Rec n m pred
-
-export
-mult : Term (N ~> N ~> N) ctx
-mult = Abs' (\n =>
-  Rec n
-    (Const Zero)
-    (Abs $ Abs $
-      let f = Var $ There Here in
-      let m = Var Here in
-      App plus [<m, App f [<m]]))
-
-export
 lte : Term (N ~> N ~> B) ctx
-lte = Abs' (\m => isZero . App minus [<m])
+lte = Abs' (\m => isZero . App (Op Minus) [<m])
 
 export
 equal : Term (N ~> N ~> B) ctx
@@ -70,17 +31,3 @@ equal = Abs $ Abs $
   let m = Var $ There Here in
   let n = Var Here in
   App and [<App lte [<m, n], App lte [<n, m]]
-
-export
-divmod : Term (N ~> N ~> N * N) ctx
-divmod = Abs $ Abs $
-  let n = Var (There Here) in
-  let d = Var Here in
-  Rec
-    n
-    (App pair [<Zero, Zero])
-    (Abs' (\p =>
-      App if'
-        [<App lte [<shift d, Suc (App snd [<p])]
-        , App pair [<Suc (App fst [<p]), Zero]
-        , App mapSnd [<Abs' Suc, p]]))