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

Agda.Utils.Either

Description

Utilities for the Either type

Synopsis

# Documentation

whileLeft :: Monad m => (a -> Either b c) -> (a -> b -> m a) -> (a -> c -> m d) -> a -> m d Source #

Loop while we have an exception.

caseEitherM :: Monad m => m (Either a b) -> (a -> m c) -> (b -> m c) -> m c Source #

Monadic version of either with a different argument ordering.

mapEither :: (a -> c) -> (b -> d) -> Either a b -> Either c d Source #

Either is a bifunctor.

mapLeft :: (a -> c) -> Either a b -> Either c b Source #

'Either _ b' is a functor.

mapRight :: (b -> d) -> Either a b -> Either a d Source #

'Either a' is a functor.

traverseEither :: Functor f => (a -> f c) -> (b -> f d) -> Either a b -> f (Either c d) Source #

Either is bitraversable.

isLeft :: Either a b -> Bool Source #

Returns True iff the argument is Left x for some x. Note: from base >= 4.7.0.0 already present in Data.Either.

isRight :: Either a b -> Bool Source #

Returns True iff the argument is Right x for some x. Note: from base >= 4.7.0.0 already present in Data.Either.

fromLeft :: (b -> a) -> Either a b -> a Source #

Analogue of fromMaybe.

fromRight :: (a -> b) -> Either a b -> b Source #

Analogue of fromMaybe.

maybeLeft :: Either a b -> Maybe a Source #

Safe projection from Left.  maybeLeft (Left a) = Just a maybeLeft Right{} = Nothing 

maybeRight :: Either a b -> Maybe b Source #

Safe projection from Right.  maybeRight (Right b) = Just b maybeRight Left{} = Nothing 

allLeft :: [Either a b] -> Maybe [a] Source #

Returns Just with tags stripped if all elements are to the Left, and otherwise Nothing.

allRight :: [Either a b] -> Maybe [b] Source #

Returns Just with tags stripped if all elements are to the right, and otherwise Nothing.

 allRight xs ==
if all isRight xs then
Just (map ((Right x) -> x) xs)
else
Nothing