Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Applicative

Synopsis

- (?*>) :: Alternative f => Bool -> f a -> f a
- (?$>) :: Alternative f => Bool -> a -> f a
- foldA :: (Alternative f, Foldable t) => t a -> f a
- foldMapA :: (Alternative f, Foldable t) => (a -> f b) -> t a -> f b
- forA :: (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)
- liftA4 :: Applicative f => (a -> b -> c -> d -> e) -> f a -> f b -> f c -> f d -> f e

# Documentation

(?*>) :: Alternative f => Bool -> f a -> f a Source #

Guard: return the action `f` only if the boolean is `True`

(?$>) :: Alternative f => Bool -> a -> f a Source #

Guard: return the value `a` only if the boolean is `True`

foldA :: (Alternative f, Foldable t) => t a -> f a Source #

Branch over a `Foldable` collection of values.

foldMapA :: (Alternative f, Foldable t) => (a -> f b) -> t a -> f b Source #

Branch over a `Foldable` collection of values using the supplied action.

forA :: (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b) Source #

Better name for `for`.

liftA4 :: Applicative f => (a -> b -> c -> d -> e) -> f a -> f b -> f c -> f d -> f e Source #