Idris2Doc : Data.Either

# Data.Either

compress : List (Eitherab) -> List (Either (List1a) (List1b))
`  Compress the list of Lefts and Rights by accumulating  all of the lefts and rights into non-empty blocks.`

Totality: total
decompress : List (Either (List1a) (List1b)) -> List (Eitherab)
`  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
eitherToMaybe : Eitherea -> Maybea
`  Convert an Either to a Maybe from Right injection`

Totality: total
fromEither : Eitheraa -> a
`  Remove a "useless" Either by collapsing the case distinction`

Totality: total
getLeft : Eitherab -> Maybea
`  Extract the Left value, if possible`

Totality: total
getRight : Eitherab -> Maybeb
`  Extract the Right value, if possible`

Totality: total
isLeft : Eitherab -> Bool
`  True if the argument is Left, False otherwise`

Totality: total
isRight : Eitherab -> Bool
`  True if the argument is Right, False otherwise`

Totality: total
leftInjective : Leftx = Lefty -> x = y
`  Left is injective`

Totality: total
lefts : List (Eitherab) -> Lista
`  Keep the payloads of all Left constructors in a list of Eithers`

Totality: total
maybeToEither : Lazy e -> Maybea -> Eitherea
`  Convert a Maybe to an Either by using a default value in case of Nothing  @ e the default value`

Totality: total
mirror : Eitherab -> Eitherba
`  Right becomes left and left becomes right`

Totality: total
partitionEithers : List (Eitherab) -> (Lista, Listb)
`  Split a list of Eithers into a list of the left elements and a list of the right elements`

Totality: total
pushInto : c -> Eitherab -> Either (c, a) (c, b)
Totality: total
rightInjective : Rightx = Righty -> x = y
`  Right is injective`

Totality: total
rights : List (Eitherab) -> Listb
`  Keep the payloads of all Right constructors in a list of Eithers`

Totality: total