feat: binder info for generalize

src/Lean/Elab/Tactic/Generalize.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Meta.Tactic.Generalize
 import Lean.Meta.Check
 import Lean.Meta.Tactic.Intro
+import Lean.Elab.Binders
 import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Location
 
@@ -14,15 +15,27 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.generalize] def evalGeneralize : Tactic := fun stx =>
   withMainContext do
-    let args ← stx[1].getSepArgs.mapM fun arg => do
-      let hName? := if arg[0].isNone then none else some arg[0][0].getId
+    let mut xIdents := #[]
+    let mut hIdents := #[]
+    let mut args := #[]
+    for arg in stx[1].getSepArgs do
+      let hName? ← if arg[0].isNone then
+        pure none
+      else
+        hIdents := hIdents.push arg[0][0]
+        pure (some arg[0][0].getId)
       let expr ← elabTerm arg[1] none
-      return { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
+      xIdents := xIdents.push arg[3]
+      args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
     let hyps ← match expandOptLocation stx[2] with
     | .targets hyps _ => getFVarIds hyps
     | .wildcard => pure (← getLCtx).getFVarIds
-    liftMetaTactic fun mvarId => do
-      let (_, _, mvarId) ← mvarId.generalizeHyp args hyps
-      return [mvarId]
+    let mvarId ← getMainGoal
+    mvarId.withContext do
+      let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps
+      mvarId.withContext do
+        for v in newVars, id in xIdents ++ hIdents do
+          Term.addLocalVarInfo id (.fvar v)
+        replaceMainGoal [mvarId]
 
 end Lean.Elab.Tactic

tests/lean/interactive/hover.lean

@@ -259,3 +259,9 @@ example : Nat :=
 
 def auto (o : Nat := by exact 1) : Nat := o
   --^ textDocument/hover
+
+example : 1 = 1 := by
+                    --v textDocument/hover
+  generalize _e : 1 = x
+           --^ textDocument/hover
+  exact Eq.refl x

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

@@ -555,3 +555,15 @@ null
  "contents":
  {"value": "```lean\nBar.auto (o : ℕ := by exact 1) : ℕ\n```",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 264, "character": 22}}
+{"range":
+ {"start": {"line": 264, "character": 22},
+  "end": {"line": 264, "character": 23}},
+ "contents": {"value": "```lean\nx : ℕ\n```", "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 264, "character": 13}}
+{"range":
+ {"start": {"line": 264, "character": 13},
+  "end": {"line": 264, "character": 15}},
+ "contents": {"value": "```lean\n_e : 1 = x\n```", "kind": "markdown"}}