feat: hover / go-to-def for attribute cmd

leanprover · Apr 13, 2024 · 93b471e · 93b471e
1 parent c24b419
commit 93b471e
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 0 deletions.
diff --git 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
@@ -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