From d684d596bcf8fbb114320776b80a1dbfce0a0786 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 27 Aug 2024 23:30:00 +0200 Subject: [PATCH] chore: remove unnecessary toList --- DocGen4/Process/Analyze.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index f9a5c7b..90191fb 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -115,7 +115,7 @@ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do let mut res ← getAllModuleDocs relevantModules.toArray - for (name, cinfo) in env.constants.toList do + for (name, cinfo) in env.constants do let some modidx := env.getModuleIdxFor? name | unreachable! let moduleName := env.allImportedModuleNames.get! modidx if !relevantModules.contains moduleName then