From e0aa9fb29072dd672a45d6e0ef9a1de449ad3b9b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Mar 2022 07:39:46 -0700 Subject: [PATCH] chore: fix typo --- src/Lean/ImportingFlag.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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