fix: use Lean.initializing instead of IO.initializing

This commit is contained in:
Mario Carneiro 2023-06-10 15:10:40 -04:00 committed by Leonardo de Moura
parent e64a2e1a12
commit 2348fb37d3
2 changed files with 2 additions and 2 deletions

View file

@ -177,7 +177,7 @@ inductive AliasValue (α : Type) where
abbrev AliasTable (α) := NameMap (AliasValue α)
def registerAliasCore {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do
unless (← IO.initializing) do throw ↑"aliases can only be registered during initialization"
unless (← initializing) do throw ↑"aliases can only be registered during initialization"
if (← mapRef.get).contains aliasName then
throw ↑s!"alias '{aliasName}' has already been declared"
mapRef.modify (·.insert aliasName value)

View file

@ -93,7 +93,7 @@ def registerBuiltinRpcProcedure (method : Name) paramType respType
[RpcEncodable paramType] [RpcEncodable respType]
(handler : paramType → RequestM (RequestTask respType)) : IO Unit := do
let errMsg := s!"Failed to register builtin RPC call handler for '{method}'"
unless (← IO.initializing) do
unless (← initializing) do
throw <| IO.userError s!"{errMsg}: only possible during initialization"
if (←builtinRpcProcedures.get).contains method then
throw <| IO.userError s!"{errMsg}: already registered"