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

Equations

• Lean.profiler.threshold.getSecs o = (Lean.Option.get o Lean.profiler.threshold).toFloat / 1000

@[extern lean_profileit]

def Lean.profileit {α : Type} (category : String) (opts : Lean.Options) (fn : Unit → α) (decl : Lean.Name := Lean.Name.anonymous) : α

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

Equations

• Lean.profileit category opts fn decl = fn ()

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

Equations

• Lean.profileitIOUnsafe category opts act decl = match Lean.profileit category opts (fun (x : Unit) => unsafeEIO act) decl with | Except.ok a => pure a | Except.error e => throw e

@[implemented_by Lean.profileitIOUnsafe]

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

Equations

• Lean.profileitIO category opts act decl = act

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

Equations

• Lean.profileitM ε category opts act decl = monadMap (fun {β : Type} (act : EIO ε β) => Lean.profileitIO category opts act decl) act