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