diff --git a/src/Lean/ImportingFlag.lean b/src/Lean/ImportingFlag.lean index e7c75ca2fd..3fc36632fa 100644 --- a/src/Lean/ImportingFlag.lean +++ b/src/Lean/ImportingFlag.lean @@ -27,7 +27,7 @@ unsafe def enableInitializersExecution : IO Unit := def isInitializerExecutionEnabled : IO Bool := runInitializersRef.get -/- We say Lean is "initializing" when it is executing `builtin_initialize` declarations and importing modules. +/- We say Lean is "initializing" when it is executing `builtin_initialize` declarations or importing modules. Recall that Lean excutes `initialize` declarations while importing modules. -/ def initializing : IO Bool := IO.initializing <||> importingRef.get