Documentation

Lean.LazyInitExtension

structure Lean.LazyInitExtension (m : TypeType) (α : Type) :
Type
instance Lean.instInhabitedLazyInitExtension {m : TypeType} {α : Type} [inst : Monad m] [inst : Inhabited α] :
Equations
  • Lean.instInhabitedLazyInitExtension = { default := { ext := default, fn := pure default } }
def Lean.registerLazyInitExtension {m : TypeType} {α : Type} (fn : m α) :
Equations
def Lean.LazyInitExtension.get {m : TypeType} {α : Type} [inst : Lean.MonadEnv m] [inst : Monad m] (init : Lean.LazyInitExtension m α) :
m α
Equations