def h.split_size

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

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

3389def h.split_size(
3390  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, n: Nat, +mask: U32, +o: U32,
3391  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, +v: V,
3392  +miss: {h.EG(~K, ~V, ~eq, es, k) == None{} : Maybe<&2, V>}
3393) -> {h.Sz(K, V, h.S(~K, ~V, ~eq, n, mask, o, es, hk, k, v)) == 1n+h.len(K, V, es) : Nat}:
3394  match n:
3395    case 0n:
3396      h.elen_put_new(~K, ~V, ~eq, es, k, v, miss)
3397    case 1n+(+p):
3398      h.split_size.b(~K, ~V, ~eq, p, mask, o, es, hk, k, v,
3399        U32.is_eq((o .&. mask : U32), (hk .&. mask : U32)), U32.is_eq((o .&. mask : U32), 0),
3400        h.split_size(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, hk, k, v, miss))