Made Ordering an Eq instance
commit9c6546e58d55839e65fd5029aea3f948b35787bb
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateTue 1 May 2012, 13:07 (14 years ago)
parent047be9e
lib/builtins.idr+6
@@ -128,6 +128,12 @@ instance (Eq a, Eq b) => Eq (a, b) where
128128
129129data Ordering = LT | EQ | GT
130130
131+instance Eq Ordering where
132+ LT == LT = True
133+ EQ == EQ = True
134+ GT == GT = True
135+ _ == _ = False
136+
131137class Eq a => Ord a where
132138 compare : a -> a -> Ordering
133139