docstrings on builtin simprocs

Consider

-- import Lean
set_option linter.unusedSimpArgs false
example : True := by simp [BitVec.reduceEq]

hovering over the simproc it just says

A simp lemma specification is:

    optional ↑ or ↓ to specify use before or after entering the subterm
    optional ← to use the lemma backward
    thm for the theorem to rewrite with

but if I add import Lean I see the more helpful

BitVec.reduceEq : Lean.Meta.Simp.Simproc

Simplification procedure for = on BitVecs.

import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

So somehow builtin simprocs don't get their docstrings show. Smells a bit like #8432, but my attempt at fixing this using

diff --git a/src/Init/Simproc.lean b/src/Init/Simproc.lean
index f188250d14..759c1a1a57 100644
--- a/src/Init/Simproc.lean
+++ b/src/Init/Simproc.lean
@@ -122,13 +122,13 @@ macro_rules
 macro_rules
   | `($[$doc?:docComment]? builtin_simproc_decl $n:ident ($pattern:term) := $body) => do
     let simprocType := `Lean.Meta.Simp.Simproc
-    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+    `($[$doc?:docComment]? @[builtin_doc] def $n:ident : $(mkIdent simprocType) := $body
       builtin_simproc_pattern% $pattern => $n)
 
 macro_rules
   | `($[$doc?:docComment]? builtin_dsimproc_decl $n:ident ($pattern:term) := $body) => do
     let simprocType := `Lean.Meta.Simp.DSimproc
-    `($[$doc?:docComment]? def $n:ident : $(mkIdent simprocType) := $body
+    `($[$doc?:docComment]? @[builtin_doc] def $n:ident : $(mkIdent simprocType) := $body
       builtin_simproc_pattern% $pattern => $n)

did not help.

Version

Lean 4.24.0-nightly-2025-09-14

Start in src/Init/Simproc.lean and inspect how builtin_simproc_decl and builtin_dsimproc_decl expand, then trace how docstrings are collected for these declarations. Reproduce the hover behavior for BitVec.reduceEq and verify that builtin simprocs display their descriptive docstrings without requiring an explicit import.