Stdlib.Data.Product.Base

Contents

type × (A : Type) (B : Type)Source #

Inductive pair. I.e. a tuple with two components.

Constructors

| , : A → B → A × B

uncurry : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> A × B -> CSource #

Converts a function of two arguments to a function with a product argument.

curry : {A : Type} -> {B : Type} -> {C : Type} -> (A × B -> C) -> A -> B -> CSource #

Converts a function with a product argument to a function of two arguments.

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.

Description

Definitions