From 55c2f88abe05c8f9a0d5c28a84949fe4cbbd91e6 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 7 Aug 2024 15:36:53 +0200 Subject: [PATCH] chore: use lexicographic sorting (#24) use lexicographic sorting --------- Co-authored-by: Moritz Firsching --- ImportGraph/Imports.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean index 970ae7e..14705b3 100644 --- a/ImportGraph/Imports.lean +++ b/ImportGraph/Imports.lean @@ -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"