max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix apply? error reporting when out of heartbeats (#6121)

Browse source
This commit is contained in:
Kim Morrison 2024-11-19 11:57:59 +11:00 • committed by GitHub
parent 799b2b6628
commit 7f0bdefb6e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Tactic/LibrarySearch.lean
View file

@ -40,7 +40,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
| some suggestions =>
if requireClose then throwError
"`exact?` could not close the goal. Try `apply?` to see partial suggestions."
reportOutOfHeartbeats `library_search ref
reportOutOfHeartbeats `apply? ref
for (_, suggestionMCtx) in suggestions do
withMCtx suggestionMCtx do
addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)