Idris2Doc : Data.Product

Data.Product

(source)
Reexports
import public Data.Ops
Definitions
record (*) : Type -> Type -> Type
  Pairs of types

  Totality: total
  Visibility: public export
  Constructor: 
(&&) : a -> b -> a * b

  Projections:
  
.p1 : a * b -> a
  
.p2 : a * b -> b

  Hints:
  
Bifunctor (*)
  
Show a => Show b => Show (a * b)

  Fixity Declaration: infixl operator, level 9
.p1 : a * b -> a
  Totality: total
  Visibility: public export
p1 : a * b -> a
  Totality: total
  Visibility: public export
.p2 : a * b -> b
  Totality: total
  Visibility: public export
p2 : a * b -> b
  Totality: total
  Visibility: public export
.π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 : {_:5830}) -> (0 b : {_:5829}) -> (a && b) .π1 = a
  Totality: total
  Visibility: public export
proj2Pair : (0 a : {_:5862}) -> (0 b : {_:5861}) -> (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