git.iko.soy/Idris-dev
on master help sign in
Merge pull request #772 from david-christiansen/either-eq
cf2eae8Edwin Brady
libs/prelude/Prelude/Either.idr+11
compare with master
unifiedsplit
@@ -63,6 +63,17 @@ maybeToEither def (Just j) = Right j
63maybeToEither def Nothing = Left def
63maybeToEither def Nothing = Left def
64
64
65
65
66+--------------------------------------------------------------------------------
67+-- Instances
68+--------------------------------------------------------------------------------
69+
70+instance (Eq a, Eq b) => Eq (Either a b) where
71+ (==) (Left x) (Left y) = x == y
72+ (==) (Right x) (Right y) = x == y
73+ (==) _ _ = False
74+
75+
76+
66--------------------------------------------------------------------------------
77--------------------------------------------------------------------------------
67-- Injectivity of constructors
78-- Injectivity of constructors
68--------------------------------------------------------------------------------
79--------------------------------------------------------------------------------