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:

Semigroup a => Applicative (These a)

Bifoldable These

Bifunctor These

Biinjective Both

Bitraversable These

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

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

Foldable (These a)

Functor (These a)

Injective This

Injective That

Injective (Both x)

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

Semigroup a => Semigroup b => Semigroup (These a b)

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

Traversable (These a)

Semigroup a => Zippable (These a)

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

fromBoth : Lazy a -> Lazy b -> These a b -> (a, b)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

these' : Lazy a -> Lazy b -> (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 : Semigroup m => These m m -> m

Totality: total
Visibility: public export