diff options
Diffstat (limited to 'src/Encoded/Arith.idr')
| -rw-r--r-- | src/Encoded/Arith.idr | 55 |
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]])) |