git.iko.soy/Idris-dev
on master help sign in
We no longer need MonadPlus, now that we've got Alternative.
e75227bstartling
lib/Prelude.idr−11
compare with master
unifiedsplit
@@ -134,13 +134,6 @@ instance Monad Maybe where
134 Nothing >>= k = Nothing
134 Nothing >>= k = Nothing
135 (Just x) >>= k = k x
135 (Just x) >>= k = k x
136
136
137−instance MonadPlus Maybe where
138− mzero = Nothing
139−
140− mplus (Just x) _ = Just x
141− mplus Nothing (Just y) = Just y
142− mplus Nothing Nothing = Nothing
143−
144instance Monad (Either e) where
137instance Monad (Either e) where
145 return = Right
138 return = Right
146
139
@@ -151,10 +144,6 @@ instance Monad List where
151 return x = [x]
144 return x = [x]
152 m >>= f = concatMap f m
145 m >>= f = concatMap f m
153
146
154−instance MonadPlus List where
155− mzero = []
156− mplus = (++)
157−
158---- some mathematical operations
147---- some mathematical operations
159
148
160%include "math.h"
149%include "math.h"
lib/Prelude/Monad.idr−4
@@ -14,10 +14,6 @@ class Applicative m => Monad (m : Type -> Type) where
14 return : a -> m a
14 return : a -> m a
15 (>>=) : m a -> (a -> m b) -> m b
15 (>>=) : m a -> (a -> m b) -> m b
16
16
17−class Monad m => MonadPlus (m : Type -> Type) where
18− mplus : m a -> m a -> m a
19− mzero : m a
20−
21mapM : Monad m => (a -> m b) -> List a -> m (List b)
17mapM : Monad m => (a -> m b) -> List a -> m (List b)
22mapM f xs = sequence (map f xs)
18mapM f xs = sequence (map f xs)
23
19