From 0bfcf434ac9637f08cce41b32a9e60972ef3b171 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Apr 2022 14:43:30 -0700
Subject: [PATCH] fix: jump to definition inside of a mutually inductive
 declaration

---
 src/Lean/Elab/Declaration.lean | 12 ++++--------
 src/Lean/Elab/Inductive.lean   |  2 ++
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 6bc030b738..77ab3344b8 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -127,18 +127,14 @@ private def inductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : Comm
     let (binders, type?) := expandOptDeclSig ctor[4]
     addDocString' ctorName ctorModifiers.docString?
     addAuxDeclarationRanges ctorName ctor ctor[2]
-    pure { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
+    return { ref := ctor, modifiers := ctorModifiers, declName := ctorName, inferMod := inferMod, binders := binders, type? := type? : CtorView }
   let classes ← getOptDerivingClasses decl[5]
-  pure {
+  return {
     ref             := decl
-    modifiers       := modifiers
     shortDeclName   := name
-    declName        := declName
-    levelNames      := levelNames
-    binders         := binders
-    type?           := type?
-    ctors           := ctors
     derivingClasses := classes
+    declId, modifiers, declName, levelNames
+    binders, type?, ctors
   }
 
 private def classInductiveSyntaxToView (modifiers : Modifiers) (decl : Syntax) : CommandElabM InductiveView :=
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 0c774e9dd6..2ec9a95a86 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -49,6 +49,7 @@ structure CtorView where
 
 structure InductiveView where
   ref             : Syntax
+  declId          : Syntax
   modifiers       : Modifiers
   shortDeclName   : Name
   declName        : Name
@@ -676,6 +677,7 @@ private def mkInductiveDecl (vars : Array Expr) (views : Array InductiveView) :
       let mut indTypesArray := #[]
       for i in [:views.size] do
         let indFVar := indFVars[i]
+        Term.addTermInfo (isBinder := true) views[i].declId indFVar
         let r       := rs[i]
         let type  ← mkForallFVars params r.type
         let ctors ← elabCtors indFVars indFVar params r