pred_eval

Mathlib.Computability.TMConfig

URI: https://scilib.ai/kg/mathlib#Turing.ToPartrec.Code.pred_eval

English

Evaluating pred yields the predecessor of the head of v as a singleton list, inside the monad.

Русский

Оценка pred даёт предшественника головы v в виде списка из одного элемента внутри монады.

LaTeX

$$$pred.eval(v) = \\operatorname{pure}([v.headI.pred])$$$

Lean4

@[simp]
theorem pred_eval (v) : pred.eval v = pure [v.headI.pred] := by simp [pred]; cases v.headI <;> simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru