diff options
| author | bringert <bringert@cs.chalmers.se> | 2005-12-02 18:33:08 +0000 |
|---|---|---|
| committer | bringert <bringert@cs.chalmers.se> | 2005-12-02 18:33:08 +0000 |
| commit | 983aef132b0695af7e1b16d77ad43180388eea71 (patch) | |
| tree | aa95e673e10ccc32e3e0fdf1556659c0c041aa53 /transfer | |
| parent | dea5158cbf1c11d45f2ed91d9975fbc77245e652 (diff) | |
Transfer added guards and Eq derivation.
Diffstat (limited to 'transfer')
| -rw-r--r-- | transfer/lib/prelude.tr | 11 |
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 |
