English
There is a standard construction uncurry that turns a function from a tuple of arguments into a function on a single argument for each index; it converts between FromTypes p τ and a function taking a vector of arguments.
Русский
Существует стандартная конструкция uncurry, превращающая функцию от кортежа аргументов в функцию по одному аргументу на каждый индекс; она переводит между FromTypes p τ и функцией, принимающей вектор аргументов.
LaTeX
$$$\\text{uncurry} : \\{n : \\mathbb{N}\\} \\to \\{p : \\mathrm{Fin}\,n \\to \\text{Type}\\} \\to \\{\\tau : \\text{Type}\\} \\to (f : \\mathrm{Function.FromTypes}\ p\\tau) \\to (i : \\mathrm{Fin}\,n) \\to p i \\to \\tau$$$
Lean4
/-- 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 uncurry : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} → (f : Function.FromTypes p τ) → ((i : Fin n) → p i) → τ
| 0, _, _, f => fun _ => f
| _ + 1, _, _, f => fun args => (f (args 0)).uncurry (args ∘' Fin.succ)
