git.iko.soy/Idris-dev
on master help sign in
You know, 'when' doesn't need Monad either.
4f93ab6startling
lib/Prelude/Applicative.idr+3
compare with master
unifiedsplit
@@ -17,3 +17,6 @@ class Applicative f => Alternative (f : Type -> Type) where
17
17
18guard : Alternative f => Bool -> f ()
18guard : Alternative f => Bool -> f ()
19guard a = if a then pure () else empty
19guard a = if a then pure () else empty
20+
21+when : Applicative f => Bool -> f () -> f ()
22+when a f = if a then f else pure ()
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−when : Monad m => Bool -> m () -> m ()
22−when True f = f
23−when False _ = return ()
24−
25sequence : Monad m => List (m a) -> m (List a)
21sequence : Monad m => List (m a) -> m (List a)
26sequence [] = return []
22sequence [] = return []
27sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]
23sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]