- 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- 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- eitherToMaybe : Either e a -> Maybe a
Convert an Either to a Maybe from Right injection
Totality: total- fromEither : Either a a -> a
Remove a "useless" Either by collapsing the case distinction
Totality: total- getLeft : Either a b -> Maybe a
Extract the Left value, if possible
Totality: total- getRight : Either a b -> Maybe b
Extract the Right value, if possible
Totality: total- isLeft : Either a b -> Bool
True if the argument is Left, False otherwise
Totality: total- isRight : Either a b -> Bool
True if the argument is Right, False otherwise
Totality: total- leftInjective : Left x = Left y -> x = y
Left is injective
Totality: total- lefts : List (Either a b) -> List a
Keep the payloads of all Left constructors in a list of Eithers
Totality: total- 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- mirror : Either a b -> Either b a
Right becomes left and left becomes right
Totality: total- 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- pushInto : c -> Either a b -> Either (c, a) (c, b)
- Totality: total
- rightInjective : Right x = Right y -> x = y
Right is injective
Totality: total- rights : List (Either a b) -> List b
Keep the payloads of all Right constructors in a list of Eithers
Totality: total