feat: term info on where declarations

src/Lean/Elab/LetRec.lean

@@ -115,6 +115,8 @@ private def registerLetRecsToLift (views : Array LetRecDeclView) (fvars : Array
 @[builtinTermElab «letrec»] def elabLetRec : TermElab := fun stx expectedType? => do
   let view ← mkLetRecDeclView stx
   withAuxLocalDecls view.decls fun fvars => do
+    for decl in view.decls, fvar in fvars do
+      addTermInfo (isBinder := true) decl.ref[0] fvar
     let values ← elabLetRecDeclValues view
     let body ← elabTermEnsuringType view.body expectedType?
     registerLetRecsToLift view.decls fvars values

tests/lean/interactive/goTo.lean

@@ -49,5 +49,6 @@ example : Nat :=
   let a := 1
 --v textDocument/definition
   a + b
+    --^ textDocument/definition
 where
   b := 2

tests/lean/interactive/goTo.lean.expected.out

@@ -96,3 +96,12 @@
   {"start": {"line": 48, "character": 6}, "end": {"line": 48, "character": 7}},
   "originSelectionRange":
   {"start": {"line": 50, "character": 2}, "end": {"line": 50, "character": 3}}}]
+{"textDocument": {"uri": "file://goTo.lean"},
+ "position": {"line": 50, "character": 6}}
+[{"targetUri": "file://goTo.lean",
+  "targetSelectionRange":
+  {"start": {"line": 53, "character": 2}, "end": {"line": 53, "character": 3}},
+  "targetRange":
+  {"start": {"line": 53, "character": 2}, "end": {"line": 53, "character": 3}},
+  "originSelectionRange":
+  {"start": {"line": 50, "character": 6}, "end": {"line": 50, "character": 7}}}]