1 | module Libraries.Decidable.Equality

 3 | import public Decidable.Equality

 5 | public export

 6 | maybeEq : DecEq a => (x, y : a) -> Maybe (x = y)

 7 | maybeEq x y = case decEq x y of

 8 |                    Yes eq => Just eq

 9 |                    No _   => Nothing

12 | public export

13 | maybeCong : (f : a -> b) -> Maybe (x = y) -> Maybe (f x = f y)

14 | maybeCong f = map (\eq => cong f eq)

17 | public export

18 | maybeCong2 : (f : a -> b -> c) -> Maybe (x = y) -> Maybe (v = w) -> Maybe (f x v = f y w)

19 | maybeCong2 f mxy mvw = (\xy, vw => cong2 f xy vw) <$> mxy <*> mvw