eval_prec_zero — Mathlib

English

In the base case, evaluating prec cf cg at pair(a,0) equals evaluating cf at a.

Русский

В базовом случае вычисления prec cf cg на пары (a,0) равно вычислению cf на a.

LaTeX

$$$\\mathrm{eval}(\\mathrm{prec} \\ cf\\ cg)(\\mathrm{pair}(a,0)) = \\mathrm{eval}(cf)(a)$$$

Lean4

/-- Helper lemma for the evaluation of `prec` in the base case. -/
@[simp]
theorem eval_prec_zero (cf cg : Code) (a : ℕ) : eval (prec cf cg) (Nat.pair a 0) = eval cf a :=
  by
  rw [eval, Nat.unpaired, Nat.unpair_pair]
  simp (config := { Lean.Meta.Simp.neutralConfig with proj := true }) only []
  rw [Nat.rec_zero]

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