Documentation

Lean.Util.Profile

@[export lean_get_profiler_threshold]
Equations
Instances For
    @[extern lean_profileit]
    def Lean.profileit {α : Type} (category : String) (opts : Lean.Options) (fn : Unitα) (decl : optParam Lake.Name Lean.Name.anonymous) :
    α

    Print and accumulate run time of act when option profiler is set to true.

    Equations
    Instances For
      unsafe def Lean.profileitIOUnsafe {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : optParam Lake.Name Lean.Name.anonymous) :
      EIO ε α
      Instances For
        @[implemented_by Lean.profileitIOUnsafe]
        def Lean.profileitIO {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : optParam Lake.Name Lean.Name.anonymous) :
        EIO ε α
        Equations
        Instances For
          def Lean.profileitM {m : TypeType} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Lean.Options) (act : m α) (decl : optParam Lake.Name Lean.Name.anonymous) :
          m α
          Equations
          Instances For