getLeft : Either a b -> Maybe a
Extract the Left value, if possible
Totality: total
Visibility: public exportgetRight : Either a b -> Maybe b
Extract the Right value, if possible
Totality: total
Visibility: public exportisLeft : Either a b -> Bool
True if the argument is Left, False otherwise
Totality: total
Visibility: public exportisRight : Either a b -> Bool
True if the argument is Right, False otherwise
Totality: total
Visibility: public exportdata 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: exportdecompress : 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: exportlefts : List (Either a b) -> List a
Keep the payloads of all Left constructors in a list of Eithers
Totality: total
Visibility: public exportrights : List (Either a b) -> List b
Keep the payloads of all Right constructors in a list of Eithers
Totality: total
Visibility: public exportpartitionEithers : 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 exportfromEither : Either a a -> a
Remove a "useless" Either by collapsing the case distinction
Totality: total
Visibility: public exportmirror : Either a b -> Either b a
Right becomes left and left becomes right
Totality: total
Visibility: public exportpushInto : 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 exporteitherToMaybe : Either e a -> Maybe a
Convert an Either to a Maybe from Right injection
Totality: total
Visibility: public exporteitherMapFusion : (f : (a -> {a:2117})) -> (g : ({b:2115} -> {a:2117})) -> (p : (b -> {b:2115})) -> (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:2215} -> {a:2221})) -> (g : ({b:2216} -> {a:2221})) -> (p : ({a:2213} -> {a:2215})) -> (q : ({b:2214} -> {b:2216})) -> (e : Either {a:2213} {b:2214}) -> either (Delay f) (Delay g) (bimap p q e) = either (Delay (f . p)) (Delay (g . q)) e
- Totality: total
Visibility: export