def Bucket.lt

bend-collections-laws-math@1.0.0.0 · spec/math/hash.bend:15

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/numeric.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/hash.bend as H

15# with mask = 2^k - 1 (the low k bits) the bucket indexes a table of 2^k
16def Bucket.lt(+w: U32, +k: Nat, +mask: U32, +hm: {mask == U32{N.mask(32n, k)} : U32}) -> Type:
17  {Nat.is_lt(U32.to_nat(H.bucket(w, mask)), N.scale_binary(k, 1n)) == True{} : Bool}