git.iko.soy/Idris-dev
on master help sign in
"guard" doesn't need MonadPlus, just Alternative.
2d17b67startling
lib/Prelude/Applicative.idr+3
compare with master
unifiedsplit
@@ -14,3 +14,6 @@ class Functor f => Applicative (f : Type -> Type) where
14class Applicative f => Alternative (f : Type -> Type) where
14class Applicative f => Alternative (f : Type -> Type) where
15 empty : f a
15 empty : f a
16 (<|>) : f a -> f a -> f a
16 (<|>) : f a -> f a -> f a
17+
18+guard : Alternative f => Bool -> f ()
19+guard a = if a then pure () else empty
lib/Prelude/Monad.idr−4
@@ -18,10 +18,6 @@ class Monad m => MonadPlus (m : Type -> Type) where
18 mplus : m a -> m a -> m a
18 mplus : m a -> m a -> m a
19 mzero : m a
19 mzero : m a
20
20
21−guard : MonadPlus m => Bool -> m ()
22−guard True = return ()
23−guard False = mzero
24−
25when : Monad m => Bool -> m () -> m ()
21when : Monad m => Bool -> m () -> m ()
26when True f = f
22when True f = f
27when False _ = return ()
23when False _ = return ()