def PW

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

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

1205# t is balanced and its weight is within one of n.
1206def PW(-K: Data, -V: Data, +n: Nat, +t: O.OMap<K, V>) -> Bool:
1207  Bool.and(WB(K, V, t), Ord.near(n, W(K, V, t)))