Prelude.Either

rights : List (Either a b) -> List b

Keep the payloads of all Right constructors in a list of Eithers

rightInjective : (Right x = Right y) -> x = y

Right is injective

partitionEithers : List (Either a b) -> (List a, List b)

Split a list of Eithers into a list of the left elements and a list of the right elements

mirror : Either a b -> Either b a

Right becomes left and left becomes right

maybeToEither : (def : Lazy e) -> Maybe a -> Either e a

Convert a Maybe to an Either by using a default value in case of Nothing

e

the default value

lefts : List (Either a b) -> List a

Keep the payloads of all Left constructors in a list of Eithers

leftInjective : (Left x = Left y) -> x = y

Left is injective

isRight : Either a b -> Bool

True if the argument is Right, False otherwise

isLeft : Either a b -> Bool

True if the argument is Left, False otherwise

fromEither : Either a a -> a

Remove a "useless" Either by collapsing the case distinction

either : (f : Lazy (a -> c)) -> (g : Lazy (b -> c)) -> (e : Either a b) -> c

Simply-typed eliminator for Either

f

the action to take on Left

g

the action to take on Right

e

the sum to analyze

data Either : (a : Type) -> (b : Type) -> Type

A sum type

Left : (l : a) -> Either a b

One possibility of the sum, conventionally used to represent errors

Right : (r : b) -> Either a b

The other possibility, conventionally used to represent success