Agda.Utils.Either

Loop while we have an exception.

Monadic version of either with a different argument ordering.

'Either _ b' is a functor.

'Either a' is a functor.

Either is bitraversable. Note: From base >= 4.10.0.0 already present in Data.Bitraversable.

Return True if the given value is a Left-value, False otherwise.

Examples

Basic usage:

>>> isLeft (Left "foo")True>>> isLeft (Right 3)False

Assuming a Left value signifies some sort of error, we can use isLeft to write a very simple error-reporting function that does absolutely nothing in the case of success, and outputs "ERROR" if any error occurred.

This example shows how isLeft might be used to avoid pattern matching when one does not care about the value contained in the constructor:

>>> import Control.Monad ( when )>>> let report e = when (isLeft e) $ putStrLn "ERROR">>> report (Right 1)>>> report (Left "parse error")ERROR

Return True if the given value is a Right-value, False otherwise.

Examples

Basic usage:

>>> isRight (Left "foo")False>>> isRight (Right 3)True

Assuming a Left value signifies some sort of error, we can use isRight to write a very simple reporting function that only outputs "SUCCESS" when a computation has succeeded.

This example shows how isRight might be used to avoid pattern matching when one does not care about the value contained in the constructor:

>>> import Control.Monad ( when )>>> let report e = when (isRight e) $ putStrLn "SUCCESS">>> report (Left "parse error")>>> report (Right 1)SUCCESS

Analogue of fromMaybe.

Analogue of fromMaybe.

Analogue of fromMaybeM.

Analogue of fromMaybeM.

Safe projection from Left.

maybeLeft (Left a) = Just a
maybeLeft Right{}  = Nothing

Safe projection from Right.

maybeRight (Right b) = Just b
maybeRight Left{}    = Nothing

Returns Just input_with_tags_stripped if all elements are to the Left, and otherwise Nothing.

Returns Just input_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

Groups a list into alternating chunks of Left and Right values

Convert Maybe to Either e, given an error e for the Nothing case.

Swap tags Left and Right.