Documentation

Lean.LazyInitExtension

structure Lean.LazyInitExtension (m : TypeType) (α : Type) :
Instances For
    Equations
    • Lean.instInhabitedLazyInitExtensionOfMonad = { default := { ext := default, fn := pure default } }
    def Lean.registerLazyInitExtension {m : TypeType} {α : Type} (fn : 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
    Instances For
      def Lean.LazyInitExtension.get {m : TypeType} {α : Type} [Lean.MonadEnv m] [Monad m] (init : Lean.LazyInitExtension m α) :
      m α
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For