structure Lean.LazyInitExtension (m : Type → Type) (α : Type) : Type

• ext : Lean.EnvExtension (Option α)
• fn : m α

instance Lean.instInhabitedLazyInitExtension {m : Type → Type} {α : Type} [Monad m] [Inhabited α] : Inhabited (Lean.LazyInitExtension m α)

Equations

• Lean.instInhabitedLazyInitExtension = { default := { ext := default, fn := pure default } }

def Lean.registerLazyInitExtension {m : Type → Type} {α : Type} (fn : m α) : IO (Lean.LazyInitExtension m α)

Register an environment extension for storing the result of fn. We initialize the extension with none, and fn is executed the first time LazyInit.get is executed.

This kind of extension is useful for avoiding work duplication in scenarios where a thunk cannot be used because the computation depends on state from the m monad. For example, we may want to "cache" a collection of theorems as a SimpLemmas object.

Equations

• Lean.registerLazyInitExtension fn = do let ext ← Lean.registerEnvExtension (pure none) pure { ext := ext, fn := fn }

def Lean.LazyInitExtension.get {m : Type → Type} {α : Type} [Lean.MonadEnv m] [Monad m] (init : Lean.LazyInitExtension m α) : m α

Equations

• One or more equations did not get rendered due to their size.