From 722b685ba7e650e82ea7f8b9f22cbcbef23dcb41 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 7 Aug 2024 15:29:08 +0200 Subject: [PATCH] typo --- ImportGraph/Imports.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ImportGraph/Imports.lean b/ImportGraph/Imports.lean index a92154b..b3209db 100644 --- a/ImportGraph/Imports.lean +++ b/ImportGraph/Imports.lean @@ -205,7 +205,7 @@ def Lean.Environment.minimalRequiredModules (env : Environment) : Array Name := let redundant := findRedundantImports env required required.filter fun n => ¬ redundant.contains n -/-- Lexikographic order of Names for sorting imports -/ +/-- Lexicographic order of Names for sorting imports -/ def sortImportsLt : Name → Name → Bool | a, b => a.toString < b.toString