Documentation

Init.Data.Function

@[inline]
def Function.curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} :
(α × βφ)αβφ
Equations
@[inline]
def Function.uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} :
(αβφ)α × βφ

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

Equations
@[simp]
theorem Function.curry_uncurry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : αβφ) :
@[simp]
theorem Function.uncurry_curry {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (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)