From 2761cd6f2c144e6118c1d1e9de093fd3b0c3d51b Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Wed, 7 Aug 2024 15:34:29 +0200
Subject: [PATCH] cleanup

---
 ImportGraph/Imports.lean | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean
index b3209db..14705b3 100644
--- a/ImportGraph/Imports.lean
+++ b/ImportGraph/Imports.lean
@@ -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.
@@ -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"