feat: term info on where declarations

leanprover · Jul 19, 2021 · 7e317d2 · 7e317d2
1 parent b76dd1a
commit 7e317d2
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 0 deletions.
diff --git a/src/Lean/Elab/LetRec.lean b/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

diff --git a/tests/lean/interactive/goTo.lean b/tests/lean/interactive/goTo.lean
@@ -49,5 +49,6 @@ example : Nat :=
   let a := 1
 --v textDocument/definition
   a + b
+    --^ textDocument/definition
 where
   b := 2
diff --git a/tests/lean/interactive/goTo.lean.expected.out b/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}}}]