PROOF.h.split_size: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 3389-3400 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=3389&end_line=3400

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

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

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shln
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.EG
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.S
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.Sz
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.elen_put_new
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.len
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&name=h.split_size.b
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/hmap.bend&name=Entry