Length_Function_is_Primitive_Recursive

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwiki

Let $n \in \N$ . Let $\map \len n$ denote the length of $n$ . Then the function $\len: \N \to \N$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Length_Function_is_Primitive_Recursive : Primrec (fun (l : List ℕ) => l.length) := by sorry

Source