English
If F is a type-valued function on a vector of length n+1, then curry F is a function that takes the first argument and the remaining n-argument vector and returns a type equal to F applied to the concatenation of the remaining vector with the first element.
Русский
Пусть F : TypeVec(n+1) → Type. Тогда curry F — это отображение, которое принимает первый аргумент и оставшийся вектор из n аргументов и возвращает параметрический тип F, применённый к конкатенации вектора оставшихся элементов с первым элементом.
LaTeX
$$$\\text{Curry}(F)(\\alpha)(\\beta) = F(\\beta ::: \\alpha).$$$
Lean4
/-- given `F : TypeVec.{u} (n+1) → Type u`, `curry F : Type u → TypeVec.{u} → Type u`,
i.e. its first argument can be fed in separately from the rest of the vector of arguments -/
def Curry (F : TypeVec.{u} (n + 1) → Type*) (α : Type u) (β : TypeVec.{u} n) : Type _ :=
F (β ::: α)
