chore: remove unnecessary toList

leanprover · Aug 27, 2024 · d684d59 · d684d59
1 parent b5c5982
commit d684d59
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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