def
MLList.whileAtLeastHeartbeatsPercent
{m : Type → Type}
{α : Type}
[Monad m]
[MonadLiftT Lean.CoreM m]
(L : MLList m α)
(percent : optParam Nat 10)
:

MLList m α

Take an initial segment of a monadic lazy list,
stopping when there is less than `percent`

of the remaining allowed heartbeats.

If `getMaxHeartbeats`

returns `0`

, then this passes through the original list unmodified.

The `initial`

heartbeat counter is recorded when the first element of the list is requested.
Then each time an element is requested from the wrapped list the heartbeat counter is checked, and
if `current * 100 / initial < percent`

then that element is returned,
but no further elements.

## Equations

- One or more equations did not get rendered due to their size.