git.iko.soy/Idris-dev
on master help sign in
Eq and Ord instances for lists and tuples.
commit7c59234829b332be301c87d49dd36db3decf8265 authorIrene Knapp <ireney.knapp@gmail.com> dateSun 22 Jan 2012, 23:54 (15 years ago) parentb21db50
2 files changed+32
compare with master
unifiedsplit
lib/builtins.idr+11 lib/prelude/list.idr+21
lib/builtins.idr+11
@@ -113,6 +113,10 @@ instance Eq Char where
113113instance Eq String where
114114 (==) = boolOp prim__eqString
115115
116+instance (Eq a, Eq b) => Eq (a, b) where
117+ (==) (a, c) (b, d) = (a == b) && (c == d)
118+
119+
116120data Ordering = LT | EQ | GT
117121
118122class Eq a => Ord a where
@@ -172,6 +176,13 @@ instance Ord String where
172176 GT
173177
174178
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+
175186class (Eq a, Ord a) => Num a where
176187 (+) : a -> a -> a
177188 (-) : a -> a -> a
lib/prelude/list.idr+21
@@ -133,3 +133,24 @@ catMaybes (x::xs) =
133133 Nothing => catMaybes xs
134134 Just j => j :: catMaybes xs
135135
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