nspec - 0.1.0

Stdlib.Data.Pair.Base

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} (f : A -> B -> C) : Pair A B -> CSource#

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

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

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

fst {A B} : Pair A B ASource#

Projects the first component of a tuple.

snd {A B} : Pair A B BSource#

Projects the second component of a tuple.

swap {A B} : Pair A B Pair B ASource#

Swaps the components of a tuple.

first {A B A'} (f : A A') : Pair A B Pair A' BSource#

Applies a function to the first component.

second {A B B'} (f : B B') : Pair A B Pair A B'Source#

Applies a function to the second component.

both {A B} (f : A B) : Pair A A Pair B BSource#

Applies a function to both components.