English
The enhance function for HAdd thunk products uses a match on the inner estimators to produce a new EstimatorData for a.prod b.
Русский
Расширяющая функция для HAdd thunk-произведения использует сопоставление по внутренним оценивателям для построения нового EstimatorData для a.prod b.
LaTeX
$$simps (EstimatorData.improve) (Prod fst snd) ...$$
Lean4
/-- Pop a `β` off the `MLList m β` with lowest priority,
also returning the index in `α` and the current best lower bound for its priority.
This may require improving estimates of priorities and shuffling the queue.
-/
partial def popWithBound (q : BestFirstQueue prio ε m β maxSize) :
m (Option (((a : α) × (ε a) × β) × BestFirstQueue prio ε m β maxSize)) := do
let q' ← ensureFirstIsBest q
match q'.minEntry? with
| none =>
-- The queue is empty, nothing to return.
return none
| some (n, l) =>
match ← l.uncons with
| none =>
-- The `MLList` associated to `n` was actually empty, so we remove `n` and try again.
popWithBound (q'.erase n)
| some (b, l') =>
-- Return the initial element `b` along with the current estimator,
-- and replace the `MLList` associated with `n` with its tail.
return some (⟨n.key, n.estimator, b⟩, q'.modify n fun _ => l')
