Documentation

Lean.Util.Profile

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

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

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