module Stdlib.Data.Pair.Base; import Stdlib.Data.Fixity open; syntax operator , pair; --- Inductive pair. I.e. a tuple with two components. builtin pair 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;