From 160c0f1fc7c9e22635522445e9cd06f1e6df3ea7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 2 Oct 2024 15:28:28 +1000 Subject: [PATCH] fix: bug in apply? when using intro --- src/Lean/Elab/Tactic/LibrarySearch.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/LibrarySearch.lean b/src/Lean/Elab/Tactic/LibrarySearch.lean index 56fcfd830316..dca70b8c1e13 100644 --- a/src/Lean/Elab/Tactic/LibrarySearch.lean +++ b/src/Lean/Elab/Tactic/LibrarySearch.lean @@ -23,7 +23,6 @@ Implementation of the `exact?` tactic. -/ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireClose : Bool) : TacticM Unit := do - let mvar ← getMainGoal let (_, goal) ← (← getMainGoal).intros goal.withContext do let required := (← (required.getD #[]).mapM getFVarId).toList.map .fvar @@ -35,7 +34,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl match ← librarySearch goal tactic allowFailure with -- Found goal that closed problem | none => - addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta + addExactSuggestion ref (← instantiateMVars (mkMVar goal)).headBeta -- Found suggestions | some suggestions => if requireClose then throwError @@ -43,7 +42,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl reportOutOfHeartbeats `library_search ref for (_, suggestionMCtx) in suggestions do withMCtx suggestionMCtx do - addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true) + addExactSuggestion ref (← instantiateMVars (mkMVar goal)).headBeta (addSubgoalsMsg := true) if suggestions.isEmpty then logError "apply? didn't find any relevant lemmas" admitGoal goal