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

Safe Haskell | None

Agda.Utils.Either

Description

Utilities for the `Either` type

Synopsis

- mapEither :: (a -> c) -> (b -> d) -> Either a b -> Either c d
- mapLeft :: (a -> c) -> Either a b -> Either c b
- mapRight :: (b -> d) -> Either a b -> Either a d
- isLeft :: Either a b -> Bool
- isRight :: Either a b -> Bool
- allRight :: [Either a b] -> Either [Either a b] [b]
- tests :: IO Bool

# Documentation

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] -> Either [Either a b] [b]

Returns ``Right` input with tags stripped` if all elements are to the right, and otherwise `Left input`:

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

tests :: IO Bool