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 : Function.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.

Equations

• x.uncurry = fun (x_1 : (i : Fin 0) → x_4 i) => x
• x.uncurry = fun (args : (i : Fin (n + 1)) → x_4 i) => (x (args 0)).uncurry ((fun {x : Fin n} => args) ∘' Fin.succ)

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

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

Equations

• Function.FromTypes.curry x = x fun (a : Fin 0) => isEmptyElim a
• Function.FromTypes.curry x = fun (a : Matrix.vecHead x_4) => Function.FromTypes.curry fun (args : (i : Fin n) → Matrix.vecTail x_4 i) => x (Fin.cons a args)

@[simp]

theorem Function.FromTypes.uncurry_apply_cons {n : ℕ} {α : Type u} {p : Fin n → Type u} {τ : Type u} (f : Function.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 : Function.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 : α) : Function.FromTypes.curry f a = Function.FromTypes.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) : Function.FromTypes.curry f a = Function.FromTypes.curry (f ∘ Fin.cons a)

@[simp]

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

@[simp]

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

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

Equiv.curry for p-ary heterogeneous functions.

Equations

• Function.FromTypes.curryEquiv p = { toFun := Function.FromTypes.curry, invFun := Function.FromTypes.uncurry, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Function.FromTypes.curryEquiv_symm_apply {n : ℕ} {τ : Type u} (p : Fin n → Type u) (f : Function.FromTypes p τ) (a✝ : (i : Fin n) → p i) : (Function.FromTypes.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) → τ) : (Function.FromTypes.curryEquiv p) a✝ = Function.FromTypes.curry a✝

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

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

def Function.OfArity.uncurry {α β : 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

• f.uncurry = Function.FromTypes.uncurry f

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

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

Equations

• Function.OfArity.curry f = Function.FromTypes.curry f

@[simp]

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

@[simp]

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

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

Equiv.curry for n-ary functions.

Equations

• Function.OfArity.curryEquiv n = Function.FromTypes.curryEquiv fun (a : Fin n) => α

@[simp]

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

@[simp]

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

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

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