curry — Mathlib

English

Fixing the first input in a code yields a code that applies the original code with that first argument fixed; curry c n = comp c (pair (Code.const n) Code.id).

Русский

Зафиксировав первый аргумент в коде, получаем код, который применяет исходный код с этим аргументом; curry c n = comp c (pair (Code.const n) Code.id).

LaTeX

$$$\\mathrm{curry}(c,n) = \\mathrm{comp} \\; c \\; (\\mathrm{pair}(\\mathrm{Code.const}(n), \\mathrm{Code.id}))$$$

Lean4

/-- Given a code `c` taking a pair as input, returns a code using `n` as the first argument to `c`.
-/
def curry (c : Code) (n : ℕ) : Code :=
  comp c (pair (Code.const n) Code.id)

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