# Documentation

Mathlib.Data.Fin.Tuple.Curry

# 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 : ) :
(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
Instances For
def Function.OfArity.curry {α : Type u} {β : Type u} {n : } (f : (Fin nα)β) :

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

Equations
Instances For
@[simp]
theorem Function.OfArity.curry_uncurry {α : Type u} {β : Type u} {n : } (f : ) :
@[simp]
theorem Function.OfArity.uncurry_curry {α : Type u} {β : Type u} {n : } (f : (Fin nα)β) :
@[simp]
theorem Function.OfArity.curryEquiv_symm_apply {α : Type u} {β : Type u} (n : ) (f : ) :
∀ (a : Fin nα), .symm f a =
@[simp]
theorem Function.OfArity.curryEquiv_apply {α : Type u} {β : Type u} (n : ) (f : (Fin nα)β) :
def Function.OfArity.curryEquiv {α : Type u} {β : Type u} (n : ) :
((Fin nα)β)

Equiv.curry for n-ary functions.

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