zero_eval

Mathlib.Computability.TMConfig

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

English

Evaluating zero on any input yields the list [0] inside the monad.

Русский

Оценка нуля на любом входе даёт список [0] внутри монады.

LaTeX

$$$zero.eval(v) = \\operatorname{pure}([0])$$$

Lean4

@[simp]
theorem zero_eval (v) : zero.eval v = pure [0] := by simp [zero]

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

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

Разделы

Аффилиация

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