module Stdlib.Data.Pair.Base;
import Stdlib.Data.Fixity open;
syntax operator , pair;
--- Inductive pair. I.e. a tuple with two components.
type Pair (A B : Type) := , : A → B → Pair A B;
--- Converts a function of two arguments to a function with a product argument.
uncurry {A B C} (f : A -> B -> C) : Pair A B -> C
| (a, b) := f a b;
--- Converts a function with a product argument to a function of two arguments.
curry {A B C} (f : Pair A B -> C) (a : A) (b : B) : C := f (a, b);
--- Projects the first component of a tuple.
fst {A B} : Pair A B → A
| (a, _) := a;
--- Projects the second component of a tuple.
snd {A B} : Pair A B → B
| (_, b) := b;
--- Swaps the components of a tuple.
swap {A B} : Pair A B → Pair B A
| (a, b) := b, a;
--- Applies a function to the first component.
first {A B A'} (f : A → A') : Pair A B → Pair A' B
| (a, b) := f a, b;
--- Applies a function to the second component.
second {A B B'} (f : B → B') : Pair A B → Pair A B'
| (a, b) := a, f b;
--- Applies a function to both components.
both {A B} (f : A → B) : Pair A A → Pair B B
| (a, b) := f a, f b;
Last modified on 2024-07-11 16:35 UTC