@[inline]

def Function.curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α × β → φ) → α → β → φ

Transforms a function from pairs into an equivalent two-parameter function.

Examples:

• Function.curry (fun (x, y) => x + y) 3 5 = 8
• Function.curry Prod.swap 3 "five" = ("five", 3)

Equations

• Function.curry f a b = f (a, b)

@[inline]

def Function.uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} : (α → β → φ) → α × β → φ

Transforms a two-parameter function into an equivalent function from pairs.

Examples:

• Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]
• [("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]

Equations

• Function.uncurry f a = f a.fst a.snd

@[simp]

theorem Function.curry_uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α → β → φ) : curry (uncurry f) = f

@[simp]

theorem Function.uncurry_curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α × β → φ) : uncurry (curry f) = f

@[simp]

theorem Function.uncurry_apply_pair {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) (x : α) (y : β) : uncurry f (x, y) = f x y

@[simp]

theorem Function.curry_apply {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) (x : α) (y : β) : curry f x y = f (x, y)