eval_part — Mathlib

English

If curry c1 n1 = curry c2 n2 then c1 = c2 and n1 = n2.

Русский

Если curry c1 n1 = curry c2 n2, то c1 = c2 и n1 = n2.

LaTeX

$$$\\forall {c_1\\ c_2\\ n_1\\ n_2},\\ (\\mathrm{curry}\\ c_1\\ n_1 = \\mathrm{curry}\\ c_2\\ n_2) \\Rightarrow (c_1 = c_2) \\wedge (n_1 = n_2)$$$

Lean4

theorem eval_part : Partrec₂ eval :=
  (Partrec.rfindOpt (primrec_evaln.to_comp.comp ((Computable.snd.pair (fst.comp fst)).pair (snd.comp fst))).to₂).of_eq
    fun a => by simp [eval_eq_rfindOpt]

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