- 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 α)
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
- Lean.LazyInitExtension.get init = do let a ← Lean.getEnv match Lean.EnvExtension.getState init.ext a with | some a => pure a | none => do let a ← init.fn Lean.modifyEnv fun env => Lean.EnvExtension.setState init.ext env (some a) pure a