Definitions
uncurry : {A : Type} -> {B : Type} -> {C : Type} -> (A -> B -> C) -> A × B -> CSource#
Converts a function of two arguments to a function with a product argument.
curry : {A : Type} -> {B : Type} -> {C : Type} -> (A × B -> C) -> A -> B -> CSource#
Converts a function with a product argument to a function of two arguments.
first : {A : Type} → {B : Type} → {A' : Type} → (A → A') → A × B → A' × BSource#
Applies a function to the first component.