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 α)

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.

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