git.iko.soy/Idris-dev
on master help sign in
Merge pull request #5 from IreneKnapp/master
32ab3b1Edwin Brady
.gitignorenew file+2
compare with master
unifiedsplit
@@ -0,0 +1,2 @@
1+dist
2+*.ibc
lib/builtins.idr+11
@@ -113,6 +113,10 @@ instance Eq Char where
113instance Eq String where
113instance Eq String where
114 (==) = boolOp prim__eqString
114 (==) = boolOp prim__eqString
115
115
116+instance (Eq a, Eq b) => Eq (a, b) where
117+ (==) (a, c) (b, d) = (a == b) && (c == d)
118+
119+
116data Ordering = LT | EQ | GT
120data Ordering = LT | EQ | GT
117
121
118class Eq a => Ord a where
122class Eq a => Ord a where
@@ -172,6 +176,13 @@ instance Ord String where
172 GT
176 GT
173
177
174
178
179+instance (Ord a, Ord b) => Ord (a, b) where
180+ compare (xl, xr) (yl, yr) =
181+ if xl /= yl
182+ then compare xl yl
183+ else compare xr yr
184+
185+
175class (Eq a, Ord a) => Num a where
186class (Eq a, Ord a) => Num a where
176 (+) : a -> a -> a
187 (+) : a -> a -> a
177 (-) : a -> a -> a
188 (-) : a -> a -> a
lib/prelude.idr−3
@@ -165,9 +165,6 @@ syntax "[" [start] "," [next] ".." [end] "]"
165
165
166---- More utilities
166---- More utilities
167
167
168−flip : (a -> b -> c) -> b -> a -> c
169−flip f x y = f y x
170−
171sum : Num a => List a -> a
168sum : Num a => List a -> a
172sum = foldl (+) 0
169sum = foldl (+) 0
173
170
lib/prelude/list.idr+28
@@ -110,6 +110,13 @@ split p xs = case break p xs of
110 (chunk, []) => [chunk]
110 (chunk, []) => [chunk]
111 (chunk, (c :: rest)) => chunk :: split p rest
111 (chunk, (c :: rest)) => chunk :: split p rest
112
112
113+any : (a -> Bool) -> List a -> Bool
114+any predicate [] = False
115+any predicate (a::rest) =
116+ if predicate a
117+ then True
118+ else any predicate rest
119+
113--------------------------------------------------------------------------------
120--------------------------------------------------------------------------------
114-- Conversions
121-- Conversions
115--------------------------------------------------------------------------------
122--------------------------------------------------------------------------------
@@ -133,3 +140,24 @@ catMaybes (x::xs) =
133 Nothing => catMaybes xs
140 Nothing => catMaybes xs
134 Just j => j :: catMaybes xs
141 Just j => j :: catMaybes xs
135
142
143+--------------------------------------------------------------------------------
144+-- Instances
145+--------------------------------------------------------------------------------
146+
147+instance (Eq a) => Eq (List a) where
148+ (==) [] [] = True
149+ (==) (a::restA) (b::restB) =
150+ if a == b
151+ then restA == restB
152+ else False
153+ (==) _ _ = False
154+
155+
156+instance Ord a => Ord (List a) where
157+ compare [] [] = EQ
158+ compare [] _ = LT
159+ compare _ [] = GT
160+ compare (a::restA) (b::restB) =
161+ if a /= b
162+ then compare a b
163+ else compare restA restB