module Stdlib.Data.Product.Base;
infixr 2 ×;
infixr 4 ,;
--- Inductive pair. I.e. a tuple with two components.
type × (A : Type) (B : Type) :=
| , : A → B → A × B;
--- Converts a function of two arguments to a function with a product argument.
uncurry : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> A × B -> C;
uncurry f (a, b) := f a b;
--- Converts a function with a product argument to a function of two arguments.
curry : {A : Type} -> {B : Type} -> {C : Type} -> (A × B -> C) -> A -> B -> C;
curry f a b := f (a, b);
--- Projects the first component of a tuple.
fst : {A : Type} → {B : Type} → A × B → A;
fst (a, _) := a;
--- Projects the second component of a tuple.
snd : {A : Type} → {B : Type} → A × B → B;
snd (_, b) := b;
--- Swaps the components of a tuple.
swap : {A : Type} → {B : Type} → A × B → B × A;
swap (a, b) := b, a;
--- Applies a function to the first component.
first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × B;
first f (a, b) := f a, b;
--- Applies a function to the second component.
second : {A : Type} → {B : Type} → {B' : Type} → (B → B') → A × B → A × B';
second f (a, b) := a, f b;
--- Applies a function to both components.
both : {A : Type} → {B : Type} → (A → B) → A × A → B × B;
both f (a, b) := f a, f b;
Last modified on 2023-05-08 11:40 UTC