Moved transfer libraries to transfer/lib

7 files changed, 40 insertions, 9 deletions

diff --git a/transfer/examples/array.tr b/transfer/lib/array.tr
index e91fe35e7..e91fe35e7 100644
--- a/transfer/examples/array.tr
+++ b/transfer/lib/array.tr
diff --git a/transfer/examples/bool.tr b/transfer/lib/bool.tr
index 401d238ef..b8c1c95a5 100644
--- a/transfer/examples/bool.tr
+++ b/transfer/lib/bool.tr
@@ -1,10 +1,4 @@
-data Bool : Type where 
-	True : Bool
-	False : Bool;
-
 depif : (A:Type) -> (B:Type) -> (b:Bool) -> A -> B -> if Type b then A else B
 depif _ _ True x _ = x
 depif _ _ False _ y = y
 
-not : Bool -> Bool
-not b = if b then False else True
diff --git a/transfer/examples/list.tr b/transfer/lib/list.tr
index 079208167..079208167 100644
--- a/transfer/examples/list.tr
+++ b/transfer/lib/list.tr
diff --git a/transfer/examples/maybe.tr b/transfer/lib/maybe.tr
index 02d7fe56d..02d7fe56d 100644
--- a/transfer/examples/maybe.tr
+++ b/transfer/lib/maybe.tr
diff --git a/transfer/examples/nat.tr b/transfer/lib/nat.tr
index c529e5238..c529e5238 100644
--- a/transfer/examples/nat.tr
+++ b/transfer/lib/nat.tr
diff --git a/transfer/examples/pair.tr b/transfer/lib/pair.tr
index 1b70411e8..1b70411e8 100644
--- a/transfer/examples/pair.tr
+++ b/transfer/lib/pair.tr
diff --git a/transfer/examples/prelude.tr b/transfer/lib/prelude.tr
index 162599e0c..cf2167c6d 100644
--- a/transfer/examples/prelude.tr
+++ b/transfer/lib/prelude.tr
@@ -14,6 +14,18 @@ id : (A:Type) -> A -> A
 id _ x = x
 
 
+--
+-- The Bool type
+--
+
+data Bool : Type where 
+	True : Bool
+	False : Bool
+
+not : Bool -> Bool
+not b = if b then False else True
+
+
 
 --
 -- The Add class
@@ -82,6 +94,31 @@ prod_Integer = rec one = 1
               	   times = prim_mul_Int
 
 
+--
+-- The Neg class
+--
+
+Neg : Type -> Type
+Neg = sig negate : A -> A
+
+negate : (A : Type) -> Neg A -> A -> A
+negate _ d = d.neg
+
+-- Operators:
+
+{-
+  (-x) => negate ? ? x
+-}
+
+-- Instances:
+
+neg_Integer : Neg Integer
+neg_Integer = rec negate = prim_neg_Int
+
+neg_Bool : Neg Bool
+neg_Bool = rec negate = not
+
+
 
 --
 -- The Eq class
@@ -145,7 +182,7 @@ ge = ordOp (\o -> case o of { LT -> False; _ -> True })
 gt : (A : Type) -> Ord A -> A -> A -> Bool
 gt = ordOp (\o -> case o of { GT -> True; _ -> False })
 
--- Operators
+-- Operators:
 
 {- 
   (x < y) => (lt ? ? x y)
@@ -154,7 +191,7 @@ gt = ordOp (\o -> case o of { GT -> True; _ -> False })
   (x > y) => (gt ? ? x y)
 -}
 
--- Instances
+-- Instances:
 
 ord_Integer : Ord Integer
 ord_Integer = rec eq = prim_eq_Int
@@ -177,7 +214,7 @@ show : (A : Type) -> Show A -> A -> String
 show _ d = d.show
 
 
--- Instances
+-- Instances:
 
 show_Integer : Show Integer
 show_Integer = rec show = prim_show_Int