Documentation

Lean.ImportingFlag

unsafe def Lean.enableInitializersExecution :

Equations

Lean.enableInitializersExecution = ST.Ref.set Lean.runInitializersRef true

def Lean.isInitializerExecutionEnabled :

Equations

Lean.isInitializerExecutionEnabled = ST.Ref.get Lean.runInitializersRef

def Lean.initializing :

Equations

Lean.initializing = (liftM IO.initializing <||> ST.Ref.get Lean.importingRef)

def Lean.withImporting {α : Type} (x : IO α) :

IO α

Equations

Lean.withImporting x = tryFinally (do ST.Ref.set Lean.importingRef true x) do ST.Ref.set Lean.importingRef false ST.Ref.set Lean.runInitializersRef false