eval_id

Mathlib.Computability.PartrecCode

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.eval_id

English

For all n, eval Code.id n = Some n.

Русский

Для всех n: eval Code.id n = Some n.

LaTeX

$$$\\forall n \\; \\mathrm{eval}(\\mathrm{Code.id}, n) = \\mathrm{Some}(n)$$$

Lean4

@[simp]
theorem eval_id (n) : eval Code.id n = Part.some n := by simp! [Seq.seq, Code.id]

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

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

Разделы

Аффилиация

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