Stdlib.Data.Product.Base
Contents
type × (A B : Type)Source#
Inductive pair. I.e. a tuple with two components.
Constructors
uncurry {A B C} (f : A -> B -> C) : A × B -> CSource#
Converts a function of two arguments to a function with a product argument.
curry {A B C} (f : A × B -> C) (a : A) (b : B) : CSource#
Converts a function with a product argument to a function of two arguments.
fst {A B} : A × B → ASource#
Projects the first component of a tuple.
snd {A B} : A × B → BSource#
Projects the second component of a tuple.
swap {A B} : A × B → B × ASource#
Swaps the components of a tuple.
first {A B A'} (f : A → A') : A × B → A' × BSource#
Applies a function to the first component.
second {A B B'} (f : B → B') : A × B → A × B'Source#
Applies a function to the second component.
both {A B} (f : A → B) : A × A → B × BSource#
Applies a function to both components.
