fix: annotate binders in intro for hover / go to def

src/Lean/Elab/Binders.lean

@@ -136,7 +136,7 @@ private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
 private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit :=
   registerCustomErrorIfMVar type ref "failed to infer binder type"
 
-private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
+def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
   addTermInfo (isBinder := true) stx fvar
 
 private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit :=

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -146,17 +146,20 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
   match stx with
-  | `(tactic| intro)                   => introStep `_
-  | `(tactic| intro $h:ident)          => introStep h.getId
-  | `(tactic| intro _)                 => introStep `_
+  | `(tactic| intro)                   => introStep none `_
+  | `(tactic| intro $h:ident)          => introStep h h.getId
+  | `(tactic| intro _%$tk)             => introStep tk `_
   | `(tactic| intro $pat:term)         => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h))
   | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
   | _ => throwUnsupportedSyntax
 where
-  introStep (n : Name) : TacticM Unit :=
-    liftMetaTactic fun mvarId => do
-      let (_, mvarId) ← Meta.intro mvarId n
-      pure [mvarId]
+  introStep (ref : Option Syntax) (n : Name) : TacticM Unit := do
+    let fvar ← liftMetaTacticAux fun mvarId => do
+      let (fvar, mvarId) ← Meta.intro mvarId n
+      pure (fvar, [mvarId])
+    if let some stx := ref then
+      withMainContext do
+        Term.addLocalVarInfo stx (mkFVar fvar)
 
 @[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
   let matchAlts := stx[1]
@@ -168,9 +171,13 @@ where
   | `(tactic| intros) => liftMetaTactic fun mvarId => do
     let (_, mvarId) ← Meta.intros mvarId
     return [mvarId]
-  | `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do
-    let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList
-    return [mvarId]
+  | `(tactic| intros $ids*) => do
+    let fvars ← liftMetaTacticAux fun mvarId => do
+      let (fvars, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList
+      return (fvars, [mvarId])
+    withMainContext do
+      for stx in ids, fvar in fvars do
+        Term.addLocalVarInfo stx (mkFVar fvar)
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx =>

tests/lean/interactive/hover.lean

@@ -141,3 +141,17 @@ example : Type 0 := Nat
 def foo.bar : Nat := 1
   --^ textDocument/hover
       --^ textDocument/hover
+
+example : Nat → Nat → Nat :=
+  fun x y =>
+    --^ textDocument/hover
+  --v textDocument/definition
+    x
+  --^ textDocument/hover
+
+example : Nat → Nat → Nat := by
+  intro x y
+      --^ textDocument/hover
+      --v textDocument/definition
+  exact x
+      --^ textDocument/hover

tests/lean/interactive/hover.lean.expected.out

@@ -179,3 +179,47 @@ null
  {"start": {"line": 140, "character": 4},
   "end": {"line": 140, "character": 11}},
  "contents": {"value": "```lean\nBar.foo.bar : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 145, "character": 6}}
+{"range":
+ {"start": {"line": 145, "character": 6}, "end": {"line": 145, "character": 7}},
+ "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 148, "character": 4}}
+[{"targetUri": "file://hover.lean",
+  "targetSelectionRange":
+  {"start": {"line": 145, "character": 6},
+   "end": {"line": 145, "character": 7}},
+  "targetRange":
+  {"start": {"line": 145, "character": 6},
+   "end": {"line": 145, "character": 7}},
+  "originSelectionRange":
+  {"start": {"line": 148, "character": 4},
+   "end": {"line": 148, "character": 5}}}]
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 148, "character": 4}}
+{"range":
+ {"start": {"line": 148, "character": 4}, "end": {"line": 148, "character": 5}},
+ "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 152, "character": 8}}
+{"range":
+ {"start": {"line": 152, "character": 8}, "end": {"line": 152, "character": 9}},
+ "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 155, "character": 8}}
+[{"targetUri": "file://hover.lean",
+  "targetSelectionRange":
+  {"start": {"line": 152, "character": 8},
+   "end": {"line": 152, "character": 9}},
+  "targetRange":
+  {"start": {"line": 152, "character": 8},
+   "end": {"line": 152, "character": 9}},
+  "originSelectionRange":
+  {"start": {"line": 155, "character": 8},
+   "end": {"line": 155, "character": 9}}}]
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 155, "character": 8}}
+{"range":
+ {"start": {"line": 155, "character": 8}, "end": {"line": 155, "character": 9}},
+ "contents": {"value": "```lean\nx : Nat\n```", "kind": "markdown"}}