@[inline]

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

Equations

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

@[inline]

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

Interpret a function with two arguments as a function on α × β

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 : α → β → φ) : Function.curry (Function.uncurry f) = f

@[simp]

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

@[simp]

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

@[simp]

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