# Additional functions using `CoreM`

state. #

def
Lean.withHeartbeats
{m : Type → Type u_1}
{α : Type}
[Monad m]
[MonadLiftT BaseIO m]
(x : m α)
:

Count the number of heartbeats used during a monadic function.

Remember that user facing heartbeats (e.g. as used in `set_option maxHeartbeats`

)
differ from the internally tracked heartbeats by a factor of 1000,
so you need to divide the results here by 1000 before comparing with user facing numbers.

## Instances For

Return the remaining heartbeats available in this computation.

## Instances For

Return the percentage of the max heartbeats allowed that have been consumed so far in this computation.

## Instances For

Log a message if it looks like we ran out of time.