Data.Product

Reexports

Definitions

record (*) : Type -> Type -> Type

  Pairs of types

Totality: total
Visibility: public export
Constructor: 

(&&) : a -> b -> a * b

Projections:

.π1 : a * b -> a

.π2 : a * b -> b

Hints:

Bifunctor (*)

Show a => Show b => Show (a * b)

Fixity Declaration: infixl operator, level 9

.π1 : a * b -> a

Totality: total
Visibility: public export

π1 : a * b -> a

Totality: total
Visibility: public export

.π2 : a * b -> b

Totality: total
Visibility: public export

π2 : a * b -> b

Totality: total
Visibility: public export

elim : (a -> a') -> (b -> b') -> (a' -> b' -> c) -> a * b -> c

Totality: total
Visibility: public export

depCurry : {0 c : a -> b -> Type} -> ((x : a) -> (y : b) -> c x y) -> (p : a * b) -> c (p .π1) (p .π2)

Totality: total
Visibility: public export

bi : (a -> x) -> (b -> y) -> a * b -> x * y

Totality: total
Visibility: public export

merge : (a -> c) -> (b -> c) -> (c -> c -> c) -> a * b -> c

  Map each element of the pair and combine the results into one

Totality: total
Visibility: public export

merge' : Monoid c => (a -> c) -> (b -> c) -> a * b -> c

  Map each element of the pair and combine the results into one using
  the monoid on `c`

Totality: total
Visibility: public export

swap : a * b -> b * a

  Swap the two elements of a product

Totality: total
Visibility: public export

toPair : a * b -> (a, b)

  Convert from a product to a pair

Totality: total
Visibility: public export

fromPair : (a, b) -> a * b

  Convert from a pair to a product

Totality: total
Visibility: public export

dup : a -> a * a

  Duplicate an element

Totality: total
Visibility: public export

distribute : a * b -> c * d -> (a * c) * (b * d)

Totality: total
Visibility: public export

fork : (a -> b) -> (a -> c) -> a -> b * c

Totality: total
Visibility: export

split : (a * b) * c -> (a * c) * (b * c)

Totality: total
Visibility: export

through : (a -> b -> c) -> (x -> y -> z) -> a * x -> b * y -> c * z

  Like bimap but with two arguments

Totality: total
Visibility: export

curry : (a * b -> c) -> a -> b -> c

  From arity 2 to arity 1 with pair

Totality: total
Visibility: public export

uncurry : (a -> b -> c) -> a * b -> c

  From arity 2 to arity 1 with pair

Totality: total
Visibility: public export

shuffle : (a * x) * (b * y) -> (a * b) * (x * y)

Totality: total
Visibility: public export

proj1Pair : (0 a : {_:5782}) -> (0 b : {_:5781}) -> (a && b) .π1 = a

Totality: total
Visibility: public export

proj2Pair : (0 a : {_:5814}) -> (0 b : {_:5813}) -> (a && b) .π2 = b

Totality: total
Visibility: public export

(^) : Type -> Nat -> Type

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 10

assocL : (a * b) * c -> a * (b * c)

Totality: total
Visibility: public export

assocR : a * (b * c) -> (a * b) * c

Totality: total
Visibility: public export

FreeProd : List Type -> Type

Totality: total
Visibility: public export

cartesian : (a, b) -> (x, y) -> ((a, x), (b, y))

Totality: total
Visibility: public export

Prod : Nat -> Type -> Type

  A product of n values of type a

Totality: total
Visibility: public export

toProduct : Vect n a -> Prod n a

  Convert a vector of n elements into a product of n values of type a

Totality: total
Visibility: export

projIdentity : (x : a * b) -> x .π1 && x .π2 = x

Totality: total
Visibility: public export

fst : a * b -> a

Totality: total
Visibility: public export

snd : a * b -> b

Totality: total
Visibility: public export