opaque Lean.profiler : Lean.Option Bool

opaque Lean.profiler.threshold : Lean.Option Nat

@[export lean_get_profiler_threshold]

def Lean.profiler.threshold.getSecs (o : Lean.Options) : Float

@[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.

unsafe def Lean.profileitIOUnsafe {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : optParam Lake.Name Lean.Name.anonymous) : EIO ε α

@[implemented_by Lean.profileitIOUnsafe]

def Lean.profileitIO {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) (decl : optParam Lake.Name Lean.Name.anonymous) : EIO ε α

def Lean.profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Lean.Options) (act : m α) (decl : optParam Lake.Name Lean.Name.anonymous) : m α