Data.These

Definitions

data These : Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

This : a -> These a b

That : b -> These a b

Both : a -> b -> These a b

Hints:

Bifoldable These

Bifunctor These

Biinjective Both

Bitraversable These

DecEq t => DecEq s => DecEq (These t s)

Eq a => Eq b => Eq (These a b)

Functor (These a)

Injective This

Injective That

Injective (Both x)

Injective (\{arg:0} => Both {arg:0} y)

(Show a, Show b) => Show (These a b)

fromEither : Either a b -> These a b

Totality: total
Visibility: public export

fromThis : These a b -> Maybe a

Totality: total
Visibility: public export

fromThat : These a b -> Maybe b

Totality: total
Visibility: public export

these : (a -> c) -> (b -> c) -> (a -> b -> c) -> These a b -> c

Totality: total
Visibility: public export

swap : These a b -> These b a

Totality: total
Visibility: public export

bifold : Monoid m => These m m -> m

Totality: total
Visibility: public export