pop — Mathlib

English

Under decidable LT and WellFoundedGT assumptions, there exists an estimator for fst of a.prod b.

Русский

При допущении decidable LT и WellFoundedGT существует оцениватель для fst от a.prod b.

LaTeX

$$instEstimatorDataFstProdOfDecidableLTOfWellFoundedGTSubtypeProdLe$$

Lean4

/-- Pop a `β` off the `MLList m β` with lowest priority.
-/
def pop (q : BestFirstQueue prio ε m β maxSize) : m (Option ((α × β) × BestFirstQueue prio ε m β maxSize)) := do
  match ← q.popWithBound with
  | none =>
    pure none
  | some (⟨a, _, b⟩, q') =>
    pure (some ((a, b), q'))

Похожие утверждения