~/jendhub

def PM

bend-kit-collections@0.1.4.1 · PROOF.bend:1062

import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
import Base
import bend-kit-collections@0.1.4.1/LAWS.bend as Laws
import bend-kit-collections@0.1.4.1/omap.bend as O

1062# What pop_min answers: its key lies between the bounds, and the rest lies above it.
1063def PM(
1064  ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>,
1065  r: K & V & O.OMap<K, V>
1066) -> Bool:
1067  (+mk, mv, t) = r
1068  Bool.and(Bool.and(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, ub, mk)),
1069    Laws.bounded(~K, ~V, ~cmp, t, Some{mk}, ub))

Uses (10)

Used by (5)