git.iko.soy/Idris-dev
on master help sign in
Eq and Ord instances for lists and tuples.
7c59234Irene Knapp
lib/builtins.idr+11
compare with master
unifiedsplit
@@ -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/list.idr+21
@@ -133,3 +133,24 @@ catMaybes (x::xs) =
133 Nothing => catMaybes xs
133 Nothing => catMaybes xs
134 Just j => j :: catMaybes xs
134 Just j => j :: catMaybes xs
135
135
136+--------------------------------------------------------------------------------
137+-- Instances
138+--------------------------------------------------------------------------------
139+
140+instance (Eq a) => Eq (List a) where
141+ (==) [] [] = True
142+ (==) (a::restA) (b::restB) =
143+ if a == b
144+ then restA == restB
145+ else False
146+ (==) _ _ = False
147+
148+
149+instance Ord a => Ord (List a) where
150+ compare [] [] = EQ
151+ compare [] _ = LT
152+ compare _ [] = GT
153+ compare (a::restA) (b::restB) =
154+ if a /= b
155+ then compare a b
156+ else compare restA restB