eval_append_singleton — Mathlib

English

The global simp lemma states that evaluating after appending a singleton equals stepping: M.eval (x ++ [a]) = M.step (M.eval x) a.

Русский

Глобальная упрощенная лемма: вычисление после добавления единичного символа равно переходу: M.eval (x ++ [a]) = M.step (M.eval x) a.

LaTeX

$$$ M.\mathrm{eval}(x \cup \{a\}) = M.\mathrm{step}(M.\mathrm{eval}(x), a) $$$

Lean4

@[simp]
theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.step (M.eval x) a :=
  evalFrom_append_singleton _ _ _ _

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