Skip to content

Commit

Permalink
fix(Linter.MinImports): remove unnecessary declarations (#18609)
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Nov 5, 2024
1 parent 426be0c commit 0c99edf
Showing 1 changed file with 5 additions and 7 deletions.
12 changes: 5 additions & 7 deletions Mathlib/Tactic/MinImports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -164,13 +164,11 @@ def getAllImports (cmd id : Syntax) (dbg? : Bool := false) :
for imp in env.header.moduleNames do
hm := hm.insert ((env.getModuleIdx? imp).getD default) imp
let mut fins : NameSet := {}
for t1 in ts do
let tns := t1::(← resolveGlobalName t1).map Prod.fst
for t in tns do
let new := match env.getModuleIdxFor? t with
| some t => (hm.get? t).get!
| none => .anonymous -- instead of `getMainModule`, we omit the current module
if !fins.contains new then fins := fins.insert new
for t in ts do
let new := match env.getModuleIdxFor? t with
| some t => (hm.get? t).get!
| none => .anonymous -- instead of `getMainModule`, we omit the current module
if !fins.contains new then fins := fins.insert new
return fins.erase .anonymous

/-- `getIrredundantImports env importNames` takes an `Environment` and a `NameSet` as inputs.
Expand Down

0 comments on commit 0c99edf

Please sign in to comment.