- ext : Lean.EnvExtension (Option α)
- fn : m α
instance
Lean.instInhabitedLazyInitExtension
{m : Type → Type}
{α : Type}
[inst : Monad m]
[inst : Inhabited α]
:
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}
[inst : Lean.MonadEnv m]
[inst : Monad m]
(init : Lean.LazyInitExtension m α)
:
m α
Equations
- One or more equations did not get rendered due to their size.