git.iko.soy/Idris-dev
on master help sign in
Add Ordering composition and use it for Ord (Vect n a)
6e49c84Melvar Chen
libs/base/Data/Vect.idr+1−5
compare with master
unifiedsplit
@@ -243,11 +243,7 @@ instance (Eq a) => Eq (Vect n a) where
243
243
244instance Ord a => Ord (Vect n a) where
244instance Ord a => Ord (Vect n a) where
245 compare [] [] = EQ
245 compare [] [] = EQ
246− compare (x::xs) (y::ys) =
246+ compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
247− if x /= y then
248− compare x y
249− else
250− compare xs ys
251
247
252
248
253--------------------------------------------------------------------------------
249--------------------------------------------------------------------------------
libs/prelude/Prelude/Classes.idr+6
@@ -71,6 +71,12 @@ instance Eq Ordering where
71 GT == GT = True
71 GT == GT = True
72 _ == _ = False
72 _ == _ = False
73
73
74+||| Compose two comparisons into the lexicographic product
75+thenCompare : Ordering -> Lazy Ordering -> Ordering
76+thenCompare LT y = LT
77+thenCompare EQ y = y
78+thenCompare GT y = GT
79+
74||| The Ord class defines comparison operations on ordered data types.
80||| The Ord class defines comparison operations on ordered data types.
75class Eq a => Ord a where
81class Eq a => Ord a where
76 compare : a -> a -> Ordering
82 compare : a -> a -> Ordering