From 93b471e5631052ecaaf62400516f5744c1abf698 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Sat, 13 Apr 2024 01:14:10 -0400
Subject: [PATCH] feat: hover / go-to-def for `attribute` cmd

---
 src/Lean/Elab/Declaration.lean    | 2 ++
 tests/lean/interactive/hover.lean | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 6f5b342f85b3..018db3f54632 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -362,6 +362,8 @@ def elabMutual : CommandElab := fun stx => do
          else
            throwUnknownConstant name
     let declName ← ensureNonAmbiguous ident declNames
+    if (← getInfoState).enabled then
+      addConstInfo ident declName
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index e8c8dfe3c46b..d70111cd031b 100644
--- a/tests/lean/interactive/hover.lean
+++ b/tests/lean/interactive/hover.lean
@@ -229,6 +229,9 @@ def my_intro : Nat := 1
                     --v textDocument/hover
 example : α → α := by my_intro _; assumption
 
+attribute [simp] my_intro
+               --^ textDocument/hover
+
 example : Nat → True := by
   intro x
       --^ textDocument/hover