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.
• Function.FromTypes.uncurry: convert an p-ary heterogeneous function to a function from (i : Fin n) → p i.
• Function.FromTypes.curry: convert a function from (i : Fin n) → p i to a p-ary heterogeneous function.

def Function.FromTypes.uncurry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : FromTypes p τ) : ((i : Fin n) → p i) → τ

Uncurry all the arguments of Function.FromTypes p τ to get a function from a tuple.

Note this can be used on raw functions if used.

def Function.FromTypes.curry {n : ℕ} {p : Fin n → Type u} {τ : Type u} : (((i : Fin n) → p i) → τ) → FromTypes p τ

Curry all the arguments of Function.FromTypes p τ to get a function from a tuple.

@[simp]

theorem Function.FromTypes.uncurry_apply_cons {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : FromTypes (Matrix.vecCons α p) τ) (a : α) (args : (i : Fin n) → p i) : f.uncurry (Fin.cons a args) = (f a).uncurry args

@[simp]

theorem Function.FromTypes.uncurry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : FromTypes p τ) (args : (i : Fin (n + 1)) → p i) : f.uncurry args = (f (args 0)).uncurry (Fin.tail args)

@[simp]

theorem Function.FromTypes.curry_apply_cons {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → Matrix.vecCons α p i) → τ) (a : α) : curry f a = curry ((fun {x : (i : Fin n) → Matrix.vecCons α p i.succ} => f) ∘' Fin.cons a)

@[simp]

theorem Function.FromTypes.curry_apply_succ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → p i) → τ) (a : p 0) : curry f a = curry (f ∘ Fin.cons a)

@[simp]

theorem Function.FromTypes.curry_uncurry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : FromTypes p τ) : curry f.uncurry = f

@[simp]

theorem Function.FromTypes.uncurry_curry {n : ℕ} {p : Fin n → Type u} {τ : Type u} (f : ((i : Fin n) → p i) → τ) : (curry f).uncurry = f

def Function.FromTypes.curryEquiv {n : ℕ} {τ : Type u} (p : Fin n → Type u) : (((i : Fin n) → p i) → τ) ≃ FromTypes p τ

Equiv.curry for p-ary heterogeneous functions.

@[simp]

theorem Function.FromTypes.curryEquiv_symm_apply {n : ℕ} {τ : Type u} (p : Fin n → Type u) (f : FromTypes p τ) (a✝ : (i : Fin n) → p i) : (curryEquiv p).symm f a✝ = f.uncurry a✝

@[simp]

theorem Function.FromTypes.curryEquiv_apply {n : ℕ} {τ : Type u} (p : Fin n → Type u) (a✝ : ((i : Fin n) → p i) → τ) : (curryEquiv p) a✝ = curry a✝

theorem Function.FromTypes.curry_two_eq_curry {p : Fin 2 → Type u} {τ : Type u} (f : ((i : Fin 2) → p i) → τ) : curry f = Function.curry (f ∘ ⇑(piFinTwoEquiv p).symm)

theorem Function.FromTypes.uncurry_two_eq_uncurry (p : Fin 2 → Type u) (τ : Type u) (f : FromTypes p τ) : f.uncurry = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)

def Function.OfArity.uncurry {α β : Type u} {n : ℕ} (f : 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.

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

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

@[simp]

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

@[simp]

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

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

Equiv.curry for n-ary functions.

@[simp]

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

@[simp]

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

theorem Function.OfArity.curry_two_eq_curry {α β : Type u} (f : (Fin 2 → α) → β) : curry f = Function.curry (f ∘ ⇑(finTwoArrowEquiv α).symm)

theorem Function.OfArity.uncurry_two_eq_uncurry {α β : Type u} (f : OfArity α β 2) : f.uncurry = Function.uncurry f ∘ ⇑(finTwoArrowEquiv α)