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