list_length — Mathlib

English

If f: α → ℕ → σ and a suitable primitive recursive g with a compatibility condition H holds, then f is primitive recursive.

Русский

Если f: α → ℕ → σ и существует подходящая примитивно вычислимая g с условием совместимости H, то f является примитивно вычислимой.

LaTeX

$$$\\forall a, n. \\text{(conditions as in the theorem)} \\Rightarrow \\mathrm{Primrec}_2 f$$$

Lean4

theorem list_length : Primrec (@List.length α) :=
  (list_foldr (@Primrec.id (List α) _) (const 0) <| to₂ <| (succ.comp <| snd.comp snd).to₂).of_eq fun l => by dsimp;
    induction l <;> simp [*]

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