@@ -69,7 +69,6 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
69 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
69 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
70 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
70 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
72−-- The believe_me is there because idris won't seem to unify (pure x = Just x) with Refl
73VerifiedMonad Maybe where
72VerifiedMonad Maybe where
74 monadApplicative Nothing Nothing = Refl
73 monadApplicative Nothing Nothing = Refl
75 monadApplicative Nothing (Just x) = Refl
74 monadApplicative Nothing (Just x) = Refl
@@ -77,7 +76,7 @@ VerifiedMonad Maybe where
77 monadApplicative (Just x) (Just y) = Refl
76 monadApplicative (Just x) (Just y) = Refl
78 monadLeftIdentity x f = Refl
77 monadLeftIdentity x f = Refl
79 monadRightIdentity Nothing = Refl
78 monadRightIdentity Nothing = Refl
80− monadRightIdentity (Just x) = (believe_me (Refl {A = Maybe a} {x = Just x}))
79+ monadRightIdentity (Just x) = Refl
81 monadAssociativity Nothing f g = Refl
80 monadAssociativity Nothing f g = Refl
82 monadAssociativity (Just x) f g = Refl
81 monadAssociativity (Just x) f g = Refl