git.iko.soy/Idris-dev
on master help sign in
Made Ordering an Eq instance
9c6546eEdwin Brady
lib/builtins.idr+6
compare with master
unifiedsplit
@@ -128,6 +128,12 @@ instance (Eq a, Eq b) => Eq (a, b) where
128
128
129data Ordering = LT | EQ | GT
129data Ordering = LT | EQ | GT
130
130
131+instance Eq Ordering where
132+ LT == LT = True
133+ EQ == EQ = True
134+ GT == GT = True
135+ _ == _ = False
136+
131class Eq a => Ord a where
137class Eq a => Ord a where
132 compare : a -> a -> Ordering
138 compare : a -> a -> Ordering
133
139