Data.Coproduct

Reexports

Definitions

data (+) : Type -> Type -> Type

  co-products

Totality: total
Visibility: public export
Constructors:

(<+) : a -> a + b

  Left choice

(+>) : b -> a + b

  Right choice

Hints:

Alternative ((() +))

Applicative ((a +))

Bifunctor (+)

Functor ((a +))

Injective (<+)

Injective (+>)

Monad ((a +))

Show a => Show b => Show (a + b)

Fixity Declaration: infixl operator, level 8

choice : (a -> c) -> (b -> c) -> a + b -> c

  Eliminator for co-products

Totality: total
Visibility: public export

dchoice : {0 m : a + b -> Type} -> ((x : a) -> m ((<+) x)) -> ((x : b) -> m ((+>) x)) -> (e : a + b) -> m e

Totality: total
Visibility: public export

dia : a + a -> a

Totality: total
Visibility: public export

Sum : Nat -> Type -> Type

  A sum of `n` values of type `a`

Totality: total
Visibility: public export

SumList : List Type -> Type

Totality: total
Visibility: public export

match : SumList a -> SumList b -> SumList (a ++ b)

Totality: total
Visibility: public export

split : SumList (a ++ b) -> SumList a + SumList b

Totality: total
Visibility: export

Selector : Nat -> Type -> Type

  A selector is a pair of a fin n and a value of type a the Fin allows to
  pick where in a sum of `n` values of `a` the value fit.

Totality: total
Visibility: public export

finToSum : Selector n a -> Sum n a

  Convert from a selector to a sum of a

Totality: total
Visibility: public export

diagonal : (n : Nat) -> Sum n a -> a

  Diagonal operator on a sum of `n` values of `a`

Totality: total
Visibility: export

sumToSelector : Sum n a -> (Fin n, a)

  Convert a sum of n values of a into a pair that records which values of `a` was in the sum in a fin

Totality: total
Visibility: export

ChoiceN : (n : Nat) -> (a -> Type) -> Sum n a -> Type

  A dependent choice from `n` values of `a`

Totality: total
Visibility: public export

diaChoice : (c : Sum n a) -> b -> ChoiceN n (const b) c

Totality: total
Visibility: export

fromMaybe : Maybe a -> () + a

Totality: total
Visibility: public export

swap : a + b -> b + a

Totality: total
Visibility: public export

alwaysLeft : a + Void -> a

  Extract the left value

Totality: total
Visibility: public export

alwaysRight : Void + b -> b

  Extract the right value

Totality: total
Visibility: public export