juvix-docs - 0.0.0

Stdlib.Data.Product.Base

Definitions

type × (A B : Type)Source#

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

Constructors

| , : A B A × B

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.