Primitive_Recursive_Function_is_Total_Recursive_Function
Provedcomputabilityprimitive-recursive-functionsproofwiki
Every primitive recursive function is a total recursive function.
Preamble
import Mathlib.Computability.Primrec import Mathlib.Computability.Partrec
Formal statement
theorem Primitive_Recursive_Function_is_Total_Recursive_Function (f : ℕ → ℕ) (hf : Nat.Primrec f) : Nat.Partrec (↑f) := by sorry
Source