def
MLList.whileAtLeastHeartbeatsPercent
{m : Type → Type}
{α : Type}
[Monad m]
[MonadLiftT Lean.CoreM m]
(L : MLList m α)
(percent : 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.