From 39f2322f35f2b2eaadb5d62aad7f09796c1ef562 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 24 Nov 2022 10:23:44 +0100
Subject: [PATCH] fix: save correct environment in info tree for `example`

---
 src/Lean/Elab/MutualDef.lean                     | 5 ++++-
 tests/lean/1018unknowMVarIssue.lean.expected.out | 5 +++--
 tests/lean/interactive/hover.lean                | 5 +++++
 tests/lean/interactive/hover.lean.expected.out   | 8 ++++++++
 4 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index c912f16d16..f9df6b46e5 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/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
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index c06d329b99..19ace5a30d 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/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⟩
diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean
index d7e10d5929..5e76ce9f7b 100644
--- a/tests/lean/interactive/hover.lean
+++ b/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
diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out
index 09c73726c6..8ca74f8449 100644
--- a/tests/lean/interactive/hover.lean.expected.out
+++ b/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"}}