Add Ordering composition and use it for Ord (Vect n a)
commit6e49c84c5e96955f44940d78fac6a48b7f62cf1e
authorMelvar Chen <Melvar.Chen@googlemail.com>
dateFri 11 Sep 2015, 01:37 (11 years ago)
parent6b4c4d2
libs/base/Data/Vect.idr+1−5
@@ -243,11 +243,7 @@ instance (Eq a) => Eq (Vect n a) where
243243
244244instance Ord a => Ord (Vect n a) where
245245 compare [] [] = EQ
246− compare (x::xs) (y::ys) =
247− if x /= y then
248− compare x y
249− else
250− compare xs ys
246+ compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys
251247
252248
253249--------------------------------------------------------------------------------
libs/prelude/Prelude/Classes.idr+6
@@ -71,6 +71,12 @@ instance Eq Ordering where
7171 GT == GT = True
7272 _ == _ = False
7373
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+
7480||| The Ord class defines comparison operations on ordered data types.
7581class Eq a => Ord a where
7682 compare : a -> a -> Ordering