Agda.Utils.Either

Utilities for the Either type

Documentation

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

Loop while we have an exception.

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

Monadic version of either with a different argument ordering.

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

Either is a bifunctor.

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

'Either _ b' is a functor.

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

'Either a' is a functor.

isLeft :: Either a b -> Bool

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

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

Analogue of fromMaybe.

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

Analogue of fromMaybe.

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

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

tests :: IO Bool