Skip to content

Commit

Permalink
chore: use lexicographic sorting (#24)
Browse files Browse the repository at this point in the history
use lexicographic sorting

---------

Co-authored-by: Moritz Firsching <[email protected]>
  • Loading branch information
joneugster and mo271 authored Aug 7, 2024
1 parent 68cd8ae commit 55c2f88
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ImportGraph/Imports.lean
Original file line number Diff line number Diff line change
Expand Up @@ -214,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 Name.lt
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 55c2f88

Please sign in to comment.