feat(Tactic/Recall): allow docstrings on recall (leanprover-community#37141)

This PR allows doc-strings to be placed before the `recall` command. The docstrings are parsed but ignored, since `recall` doesn't introduce a new declaration. This is useful when `recall` is used in expository files where surrounding declarations have docstrings.

🤖 Prepared with Claude Code

Author: kim-em

Mathlib/Tactic/Recall.lean

@@ -36,13 +36,19 @@ capture some details (like binders), so the following works without error.
 ```
 recall Nat.add_comm {n m : Nat} : n + m = m + n
 ```
+
+Docstrings are permitted but are ignored:
+```
+/-- The additive commutativity of natural numbers. -/
+recall Nat.add_comm (n m : Nat) : n + m = m + n
+```
 -/
-syntax (name := recall) "recall " ident ppIndent(optDeclSig) (declVal)? : command
+syntax (name := recall) (docComment)? "recall " ident ppIndent(optDeclSig) (declVal)? : command
 
 open Lean Meta Elab Command Term
 
 elab_rules : command
-  | `(recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
+  | `($[$_doc?:docComment]? recall $id $sig:optDeclSig $[$val?]?) => withoutModifyingEnv do
     let declName := id.getId
     addConstInfo id declName
     let info ← getConstInfo declName

MathlibTest/Recall.lean

@@ -93,3 +93,6 @@ axiom bar : Nat
 #guard_msgs in recall bar := bar
 
 recall List.cons_append (a : α) (as bs : List α) : (a :: as) ++ bs = a :: (as ++ bs) := rfl
+
+/-- Recalling `Nat.add_comm`. -/
+recall Nat.add_comm (n m : Nat) : n + m = m + n