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]