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

Agda.Utils.Either

Description

Utilities for the `Either` type

Synopsis

- isLeft :: Either a b -> Bool
- isRight :: Either a b -> Bool
- allRight :: [Either a b] -> Either [Either a b] [b]
- tests :: IO Bool

# Documentation

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