nspec - 0.1.1

Stdlib.Data.Pair.Base

Description

Definitions

builtin pair type Pair (A B : Type)Source#

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

Constructors

| , : A → B → Pair A B

uncurry {A B C} (fun : A -> B -> C) (pair : Pair A B) : CSource#

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

curry {A B C} (fun : Pair A B -> C) (a : A) (b : B) : CSource#

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

fst {A B} (pair : Pair A B) : ASource#

Projects the first component of a tuple.

snd {A B} (pair : Pair A B) : BSource#

Projects the second component of a tuple.

swap {A B} (pair : Pair A B) : Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (fun : A -> A') (pair : Pair A B) : Pair A' BSource#

Applies a function f to the first component.

second {A B B'} (fun : B -> B') (pair : Pair A B) : Pair A B'Source#

Applies a function f to the second component.

both {A B} (fun : A -> B) (pair : Pair A A) : Pair B BSource#

Applies a function f to both components.