summaryrefslogtreecommitdiff
path: root/transfer
diff options
context:
space:
mode:
authorbringert <bringert@cs.chalmers.se>2005-12-02 18:33:08 +0000
committerbringert <bringert@cs.chalmers.se>2005-12-02 18:33:08 +0000
commit983aef132b0695af7e1b16d77ad43180388eea71 (patch)
treeaa95e673e10ccc32e3e0fdf1556659c0c041aa53 /transfer
parentdea5158cbf1c11d45f2ed91d9975fbc77245e652 (diff)
Transfer added guards and Eq derivation.
Diffstat (limited to 'transfer')
-rw-r--r--transfer/lib/prelude.tr11
1 files changed, 10 insertions, 1 deletions
diff --git a/transfer/lib/prelude.tr b/transfer/lib/prelude.tr
index 7602ea4d5..a9ec4812b 100644
--- a/transfer/lib/prelude.tr
+++ b/transfer/lib/prelude.tr
@@ -19,6 +19,10 @@ flip _ _ _ f x y = f y x
compose : (A:Type) -> (B:Type) -> (C:Type) -> (B -> C) -> (A -> B) -> A -> C
compose _ _ _ f g x = f (g x)
+otherwise : Bool
+otherwise = True
+
+
--
-- The Integer type
--
@@ -133,6 +137,11 @@ map : (A:Type) -> (B:Type) -> (A -> B) -> List A -> List B
map _ _ _ [] = []
map A B f (x::xs) = f x :: map A B f xs
+filter : (A:Type) -> (A -> Bool) -> List A -> List A
+filter _ _ [] = []
+filter A f (x::xs) | f x = x :: filter A f xs
+filter A f (x::xs) = filter A f xs
+
append : (A:Type) -> List A -> List A -> List A
append A xs ys = foldr A (List A) (Cons A) ys xs
@@ -165,7 +174,7 @@ data Maybe : Type -> Type where
Just : (A : Type) -> A -> Maybe A
-- derive Show Maybe
--- derive Eq Maybe
+derive Eq Maybe
-- derive Ord Maybe