Currying and uncurrying of n-ary functions

A function of n arguments can either be written as f a₁ a₂ ⋯ aₙ or f' ![a₁, a₂, ⋯, aₙ]. This file provides the currying and uncurrying operations that convert between the two, as n-ary generalizations of the binary curry and uncurry.

Main definitions

• Function.OfArity.uncurry: convert an n-ary function to a function from Fin n → α.
• Function.OfArity.curry: convert a function from Fin n → α to an n-ary function.

def Function.OfArity.uncurry {α : Type u} {β : Type u} {n : ℕ} (f : Function.OfArity α β n) : (Fin n → α) → β

Uncurry all the arguments of Function.OfArity α n to get a function from a tuple.

Note this can be used on raw functions if used

Equations

• Function.OfArity.uncurry f_2 = fun (x : Fin 0 → α) => f_2
• Function.OfArity.uncurry f_2 = fun (args : Fin (n_2 + 1) → α) => Function.OfArity.uncurry (f_2 (args 0)) (args ∘ Fin.succ)

def Function.OfArity.curry {α : Type u} {β : Type u} {n : ℕ} (f : (Fin n → α) → β) : Function.OfArity α β n

Uncurry all the arguments of Function.OfArity α β n to get a function from a tuple.

Equations

• Function.OfArity.curry f_2 = f_2 Fin.elim0
• Function.OfArity.curry f_2 = fun (a : α) => Function.OfArity.curry fun (args : Fin (Nat.add n_2 0) → α) => f_2 (Fin.cons a args)

@[simp]

theorem Function.OfArity.curry_uncurry {α : Type u} {β : Type u} {n : ℕ} (f : Function.OfArity α β n) : Function.OfArity.curry (Function.OfArity.uncurry f) = f

@[simp]

theorem Function.OfArity.uncurry_curry {α : Type u} {β : Type u} {n : ℕ} (f : (Fin n → α) → β) : Function.OfArity.uncurry (Function.OfArity.curry f) = f

@[simp]

theorem Function.OfArity.curryEquiv_symm_apply {α : Type u} {β : Type u} (n : ℕ) (f : Function.OfArity α β n) : ∀ (a : Fin n → α), (Function.OfArity.curryEquiv n).symm f a = Function.OfArity.uncurry f a

@[simp]

theorem Function.OfArity.curryEquiv_apply {α : Type u} {β : Type u} (n : ℕ) (f : (Fin n → α) → β) : (Function.OfArity.curryEquiv n) f = Function.OfArity.curry f

def Function.OfArity.curryEquiv {α : Type u} {β : Type u} (n : ℕ) : ((Fin n → α) → β) ≃ Function.OfArity α β n

Equiv.curry for n-ary functions.

Equations

• One or more equations did not get rendered due to their size.