zero'_eval

Mathlib.Computability.TMConfig

URI: https://scilib.ai/kg/mathlib#Turing.ToPartrec.Code.zero'_eval

English

The evaluation of zero' simply prepends a 0 to the input: zero'.eval = v ↦ pure (0 :: v).

Русский

Оценка нуль-перехода просто добавляет 0 в начало входа: zero'.eval = v ↦ pure (0 :: v).

LaTeX

$$$$ \\text{zero}'\\,.\\text{eval} = \\text{fun } v \\mapsto \\text{pure} (0 \\;:\\; v). $$$$

Lean4

@[simp]
theorem zero'_eval : zero'.eval = fun v => pure (0 :: v) := by simp [eval]

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

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

Разделы

Аффилиация

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