id_eval

Mathlib.Computability.TMConfig

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

English

Evaluating the identity code returns the input unchanged, inside the monad.

Русский

Оценка кодa-идентичности возвращает вход без изменений внутри монадического контекста.

LaTeX

$$$(id).eval(v) = \\operatorname{pure}(v)$$$

Lean4

@[simp]
theorem id_eval (v) : id.eval v = pure v := by simp [id]

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

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

Разделы

Аффилиация

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