@[extern lean_profileit]
Equations
- Lean.profileit category opts fn = fn ()
unsafe def
Lean.profileitIOUnsafe
{ε : Type}
{α : Type}
(category : String)
(opts : Lean.Options)
(act : EIO ε α)
:
EIO ε α
Equations
- Lean.profileitIOUnsafe category opts act = match Lean.profileit category opts fun x => unsafeEIO act with | Except.ok a => pure a | Except.error e => throw e
@[implementedBy Lean.profileitIOUnsafe]
noncomputable def
Lean.profileitIO
{ε : Type}
{α : Type}
(category : String)
(opts : Lean.Options)
(act : EIO ε α)
:
EIO ε α
Equations
- Lean.profileitIO category opts act = act
def
Lean.profileitM
{m : Type → Type}
(ε : Type)
[inst : MonadFunctorT (EIO ε) m]
{α : Type}
(category : String)
(opts : Lean.Options)
(act : m α)
:
m α
Equations
- Lean.profileitM ε category opts act = monadMap (fun {β} => Lean.profileitIO category opts) act