diff --git a/tests/lean/run/printDecls.lean b/tests/lean/run/printDecls.lean
index 81635a13c4..b6b4ddf41d 100644
--- a/tests/lean/run/printDecls.lean
+++ b/tests/lean/run/printDecls.lean
@@ -15,8 +15,12 @@ def printDecls (pre : Name) : MetaM Unit := do
   let cs := (← getEnv).constants
   cs.forM fun declName info => do
     if pre.isPrefixOf declName && !shouldIgnore declName then
-      IO.println s!"{declName} : {← ppExpr info.type}"
+      if let some docString := findDocString? (← getEnv) declName then
+        IO.println s!"/-- {docString} -/\n{declName} : {← ppExpr info.type}"
+      else
+        IO.println s!"{declName} : {← ppExpr info.type}"
 
 #eval printDecls `Array
 #eval printDecls `List
 #eval printDecls `Bool
+#eval printDecls `Lean.Elab