fix: save correct environment in info tree for example

src/Lean/Elab/MutualDef.lean

@@ -761,7 +761,10 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
 
 def elabMutualDef (vars : Array Expr) (views : Array DefView) (hints : TerminationHints) : TermElabM Unit :=
   if isExample views then
-    withoutModifyingEnv go
+    withoutModifyingEnv do
+      -- save correct environment in info tree
+      withSaveInfoContext do
+        go
   else
     go
 where

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -33,8 +33,9 @@ a : α
       • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
       • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
       • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-      • _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
-          n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+      • match α, β, x, a with
+        | α_1, .(α_1), Fam2.any, a => ?m x α_1 a
+        | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
         • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent
           • [.] `x : none @ ⟨8, 8⟩-⟨8, 9⟩
           • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩

tests/lean/interactive/hover.lean

@@ -251,3 +251,8 @@ example : Nat → Nat
 example : Inhabited Nat := ⟨Nat.zero⟩
                          --^ textDocument/hover
                           --^ textDocument/hover
+
+example : Nat :=
+  let x := match 0 with | _ => 0
+  _
+--^ textDocument/hover

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

@@ -540,3 +540,11 @@ null
  {"value":
   "```lean\nNat.zero : ℕ\n```\n***\n`Nat.zero`, normally written `0 : Nat`, is the smallest natural number.\nThis is one of the two constructors of `Nat`. \n***\n*import Init.Prelude*",
   "kind": "markdown"}}
+{"textDocument": {"uri": "file://hover.lean"},
+ "position": {"line": 256, "character": 2}}
+{"range":
+ {"start": {"line": 256, "character": 2}, "end": {"line": 256, "character": 3}},
+ "contents":
+ {"value":
+  "```lean\nlet x :=\n  match 0 with\n  | x => 0;\nℕ\n```\n***\nA placeholder term, to be synthesized by unification. ",
+  "kind": "markdown"}}