Documentation

Lean.Util.Profile

@[extern lean_profileit]
def Lean.profileit {α : Type} (category : String) (opts : Lean.Options) (fn : Unitα) :
α
Equations
unsafe def Lean.profileitIOUnsafe {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) :
EIO ε α
Equations
@[implementedBy Lean.profileitIOUnsafe]
noncomputable def Lean.profileitIO {ε : Type} {α : Type} (category : String) (opts : Lean.Options) (act : EIO ε α) :
EIO ε α
Equations
def Lean.profileitM {m : TypeType} (ε : Type) [inst : MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Lean.Options) (act : m α) :
m α
Equations