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

refactor: TerminationHint: Remove duplicted code line (#2859)

Browse source 
(I sincerely hope that erasing from a map is idempotent :-))
This commit is contained in:
Joachim Breitner 2023-11-10 17:17:27 +01:00 • committed by GitHub
parent 5189578a48
commit fd0a209f74
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
View file

@ -53,7 +53,6 @@ def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : Ter
| TerminationHint.many m => Id.run do
for declName in clique do
if m.contains declName then
let m := m.erase declName
let m := m.erase declName
if m.isEmpty then
return TerminationHint.none