eval_const

Mathlib.Computability.PartrecCode

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

English

For all n,m, eval(Code.const n) m = Some n.

Русский

Для любых n,m: eval(Code.const n) m = Some(n).

LaTeX

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

Lean4

@[simp]
theorem eval_const : ∀ n m, eval (Code.const n) m = Part.some n
  | 0, _ => rfl
  | n + 1, m => by simp! [eval_const n m]

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

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

Разделы

Аффилиация

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