Idris2Doc : Data.Either

# Data.Either

## Reexports

`import public Control.Function`

## 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