curry — Mathlib

English

Curry all the arguments of a function of arity n to obtain a function from Fin n to α to β; i.e., a one-to-one correspondence between n-ary functions and curried functions.

Русский

Карри все аргументы функции арности n, чтобы получить функцию от Fin n к α к β; то есть существует биекция между n-арными функциями и их карри-аналоги.

LaTeX

$$$\operatorname{curry}_{n} : ((\mathrm{Fin}\ n \to \alpha) \to \beta) \to \mathrm{Function.OfArity}\; \alpha\; \beta\; n$$$

Lean4

/-- Curry all the arguments of `Function.OfArity α β n` to get a function from a tuple. -/
def curry {n} (f : (Fin n → α) → β) : Function.OfArity α β n :=
  FromTypes.curry f

Похожие утверждения