doc: eval is a universal partial recursive function (#9703)

Mathlib/Computability/PartrecCode.lean

@@ -695,7 +695,8 @@ theorem smn :
   ⟨curry, Primrec₂.to_comp curry_prim, eval_curry⟩
 #align nat.partrec.code.smn Nat.Partrec.Code.smn
 
-/-- A function is partial recursive if and only if there is a code implementing it. -/
+/-- A function is partial recursive if and only if there is a code implementing it. Therefore,
+`eval` is a **universal partial recursive function**. -/
 theorem exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ c : Code, eval c = f := by
   refine ⟨fun h => ?_, ?_⟩
   · induction h with