- data Either : (a : Type) ->
(b : Type) ->
Type
A sum type
- Left : (l : a) ->
Either a
b
One possibility of the sum, conventionally used to represent errors
- Right : (r : b) ->
Either a
b
The other possibility, conventionally used to represent success
- either : (f : Lazy (a ->
c)) ->
(g : Lazy (b ->
c)) ->
(e : Either a
b) ->
c
Simply-typed eliminator for Either
- f
the action to take on Left
- g
the action to take on Right
- e
the sum to analyze
- eitherToMaybe : Either e
a ->
Maybe a
Convert an Either to a Maybe from Right injection
- fromEither : Either a
a ->
a
Remove a "useless" Either by collapsing the case distinction
- isLeft : Either a
b ->
Bool
True if the argument is Left, False otherwise
- isRight : Either a
b ->
Bool
True if the argument is Right, False otherwise
- leftInjective : (Left x =
Left y) ->
x =
y
Left is injective
- lefts : List (Either a
b) ->
List a
Keep the payloads of all Left constructors in a list of Eithers
- maybeToEither : (def : 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
- mirror : Either a
b ->
Either b
a
Right becomes left and left becomes right
- 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
- rightInjective : (Right x =
Right y) ->
x =
y
Right is injective
- rights : List (Either a
b) ->
List b
Keep the payloads of all Right constructors in a list of Eithers