e75227b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

We no longer need MonadPlus, now that we've got Alternative.

commite75227be5fec7a507eed4952686b1feadaa682cc authorstartling <tdixon51793@gmail.com> dateThu 13 Dec 2012, 21:21 (14 years ago) parent583c726

2 files changed−15

unifiedsplit

lib/Prelude.idr−11

@@ -134,13 +134,6 @@ instance Monad Maybe where

134134 Nothing >>= k = Nothing

135135 (Just x) >>= k = k x

136136

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−

144137instance Monad (Either e) where

145138 return = Right

146139

@@ -151,10 +144,6 @@ instance Monad List where

151144 return x = [x]

152145 m >>= f = concatMap f m

153146

154−instance MonadPlus List where

155− mzero = []

156− mplus = (++)

157−

158147---- some mathematical operations

159148

160149%include "math.h"

lib/Prelude/Monad.idr−4

@@ -14,10 +14,6 @@ class Applicative m => Monad (m : Type -> Type) where

1414 return : a -> m a

1515 (>>=) : m a -> (a -> m b) -> m b

1616

17−class Monad m => MonadPlus (m : Type -> Type) where

18− mplus : m a -> m a -> m a

19− mzero : m a

20−

2117mapM : Monad m => (a -> m b) -> List a -> m (List b)

2218mapM f xs = sequence (map f xs)

2319