eval_curry — Mathlib

English

Let c be a code and n, x be natural numbers. Then evaluating the curry of c with n at x gives the same result as evaluating c at the paired input (n, x): eval(curry c n) x = eval c (pair n x).

Русский

Пусть c — код, а n, x — натуральные числа. Тогда вычисление карри c с аргументом n на входе x даёт тот же результат, что и вычисление c на пары (n, x): eval(curry c n) x = eval c (pair n x).

LaTeX

$$$\\forall c\\,\\forall n\\,\\forall x\\; (\\mathrm{eval}(\\mathrm{curry}\\ c\\ n))(x) = (\\mathrm{eval}\,c)(\\mathrm{pair}(n,x))$$$

Lean4

@[simp]
theorem eval_curry (c n x) : eval (curry c n) x = eval c (Nat.pair n x) := by simp! [Seq.seq, curry]

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