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.

isRight :: Either a b -> Bool

Returns True iff the argument is Right x for some x.

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