primrec_const — Mathlib

English

The function that maps a natural number n to the code Code.const n is primitive recursive.

Русский

Функция, отправляющая натуральное число n в код Code.const n, является примитивно вычислимой.

LaTeX

$$$\\mathrm{Primrec}\\; \\mathrm{Code.const}$$$

Lean4

theorem primrec_const : Primrec Code.const :=
  (_root_.Primrec.id.nat_iterate (_root_.Primrec.const zero)
        (primrec₂_comp.comp (_root_.Primrec.const succ) Primrec.snd).to₂).of_eq
    fun n => by simp; induction n <;> simp [*, Code.const, Function.iterate_succ', -Function.iterate_succ]

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