summaryrefslogtreecommitdiff
path: root/transfer/lib/nat.tra
diff options
context:
space:
mode:
Diffstat (limited to 'transfer/lib/nat.tra')
-rw-r--r--transfer/lib/nat.tra24
1 files changed, 0 insertions, 24 deletions
diff --git a/transfer/lib/nat.tra b/transfer/lib/nat.tra
deleted file mode 100644
index b13a809ed..000000000
--- a/transfer/lib/nat.tra
+++ /dev/null
@@ -1,24 +0,0 @@
-import prelude
-
-data Nat : Type where
- Zero : Nat
- Succ : (n:Nat) -> Nat
-
-add_Nat : Add Nat
-add_Nat = rec zero = Zero
- plus = natPlus
-
-natPlus : Nat -> Nat -> Nat
-natPlus Zero y = y
-natPlus (Succ x) y = Succ (natPlus x y)
-
-pred : Nat -> Nat
-pred Zero = Zero
-pred (Succ n) = n
-
-natToInt : Nat -> Integer
-natToInt Zero = 0
-natToInt (Succ n) = 1 + natToInt n
-
-intToNat : Integer -> Nat
-intToNat n = if n == 0 then Zero else Succ (intToNat (n-1))