Data.Either

Reexports

Definitions

getLeft : Either a b -> Maybe a

  Extract the Left value, if possible

Totality: total
Visibility: public export

getRight : Either a b -> Maybe b

  Extract the Right value, if possible

Totality: total
Visibility: public export

isLeft : Either a b -> Bool

  True if the argument is Left, False otherwise

Totality: total
Visibility: public export

isRight : Either a b -> Bool

  True if the argument is Right, False otherwise

Totality: total
Visibility: public export

data IsRight : Either a b -> Type

  Proof that an `Either` is actually a Right value

Totality: total
Visibility: public export
Constructor: 

ItIsRight : IsRight (Right x)

Hint: 

Uninhabited (IsRight (Left x))

data IsLeft : Either a b -> Type

  Proof that an `Either` is actually a Left value

Totality: total
Visibility: public export
Constructor: 

ItIsLeft : IsLeft (Left x)

Hint: 

Uninhabited (IsLeft (Right x))

compress : List (Either a b) -> List (Either (List1 a) (List1 b))

  Compress the list of Lefts and Rights by accumulating
  all of the lefts and rights into non-empty blocks.

Totality: total
Visibility: export

decompress : List (Either (List1 a) (List1 b)) -> List (Either a b)

  Decompress a compressed list. This is the left inverse of `compress` but not its
  right inverse because nothing forces the input to be maximally compressed!

Totality: total
Visibility: export

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

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

Totality: total
Visibility: public export

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

fromEither : Either a a -> a

  Remove a "useless" Either by collapsing the case distinction

Totality: total
Visibility: public export

mirror : Either a b -> Either b a

  Right becomes left and left becomes right

Totality: total
Visibility: public export

pushInto : c -> Either a b -> Either (c, a) (c, b)

Totality: total
Visibility: export

maybeToEither : 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

Totality: total
Visibility: public export

eitherToMaybe : Either e a -> Maybe a

  Convert an Either to a Maybe from Right injection

Totality: total
Visibility: public export

eitherMapFusion : (f : (a -> {a:4822})) -> (g : ({b:4820} -> {a:4822})) -> (p : (b -> {b:4820})) -> (e : Either a b) -> either (Delay f) (Delay g) (map p e) = either (Delay f) (Delay (g . p)) e

Totality: total
Visibility: export

eitherBimapFusion : (f : ({a:4920} -> {a:4926})) -> (g : ({b:4921} -> {a:4926})) -> (p : ({a:4918} -> {a:4920})) -> (q : ({b:4919} -> {b:4921})) -> (e : Either {a:4918} {b:4919}) -> either (Delay f) (Delay g) (bimap p q e) = either (Delay (f . p)) (Delay (g . q)) e

Totality: total
Visibility: export