docs

leanprover-community · Oct 28, 2024 · 894f7a8 · 894f7a8
1 parent 7211477
commit 894f7a8
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Tactic/Linter/MinImports.lean b/Mathlib/Tactic/Linter/MinImports.lean
@@ -35,8 +35,12 @@ namespace Mathlib.Linter
 * `importSize` is the number of transitive imports to build the file up to the current command.
 -/
 structure ImportState where
+  /-- The transitive closure of the import graph of the current file.  The value is `none` only at
+  initialization time, as the linter immediately sets it to its value for the current file. -/
   transClosure : Option (NameMap NameSet) := none
+  /-- The minimal imports needed to build the file up to the current command. -/
   minImports   : NameSet := {}
+  /-- The number of transitive imports needed to build the file up to the current command. -/
   importSize   : Nat := 0
   deriving Inhabited