Skip to content

Commit

Permalink
cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Aug 7, 2024
1 parent 722b685 commit 2761cd6
Showing 1 changed file with 1 addition and 5 deletions.
6 changes: 1 addition & 5 deletions ImportGraph/Imports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -205,10 +205,6 @@ def Lean.Environment.minimalRequiredModules (env : Environment) : Array Name :=
let redundant := findRedundantImports env required
required.filter fun n => ¬ redundant.contains n

/-- Lexicographic order of Names for sorting imports -/
def sortImportsLt : Name → Name → Bool
| a, b => a.toString < b.toString

/--
Try to compute a minimal set of imports for this file,
by analyzing the declarations.
Expand All @@ -218,7 +214,7 @@ and is not aware of syntax and tactics,
so the results will likely need to be adjusted by hand.
-/
elab "#min_imports" : command => do
let imports := (← getEnv).minimalRequiredModules.qsort sortImportsLt
let imports := (← getEnv).minimalRequiredModules.qsort (·.toString < ·.toString)
|>.toList.map (fun n => "import " ++ n.toString)
logInfo <| Format.joinSep imports "\n"

Expand Down

0 comments on commit 2761cd6

Please sign in to comment.