fix: show expected type in term goal

leanprover · Jun 7, 2021 · f5f9be1 · f5f9be1
1 parent 960cfd9
commit f5f9be1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
@@ -479,7 +479,7 @@ section RequestHandling
         for t in snap.cmdState.infoState.trees do
           if let some (ci, Info.ofTermInfo i) := t.termGoalAt? hoverPos then
             let goal ← ci.runMetaM i.lctx <| open Meta in do
-              let ty ← instantiateMVars <|<- inferType i.expr
+              let ty ← instantiateMVars <| i.expectedType?.getD (← inferType i.expr)
               withPPInaccessibleNames <| Meta.ppGoal (← mkFreshExprMVar ty).mvarId!
             let range := if hasRange i.stx then rangeOfSyntax! text i.stx else ⟨p.position, p.position⟩
             return some { goal := toString goal, range }

diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out
@@ -17,7 +17,7 @@
  "position": {"line": 2, "character": 29}}
 {"range":
  {"start": {"line": 2, "character": 28}, "end": {"line": 2, "character": 46}},
- "goal": "⊢ 1 < Nat.succ 1"}
+ "goal": "⊢ 1 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 44}}
 {"range":
@@ -27,7 +27,7 @@
  "position": {"line": 11, "character": 10}}
 {"range":
  {"start": {"line": 11, "character": 10}, "end": {"line": 11, "character": 18}},
- "goal": "y : Int\n⊢ Nat"}
+ "goal": "y : Int\n⊢ OptionM Nat"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 16, "character": 16}}
 {"range":
@@ -57,4 +57,4 @@
  "position": {"line": 31, "character": 8}}
 {"range":
  {"start": {"line": 31, "character": 8}, "end": {"line": 31, "character": 24}},
- "goal": "n : Nat\n⊢ n < Nat.succ n"}
+ "goal": "n : Nat\n⊢ n < n + 1"}