LAWS.omap_weight: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/LAWS.bend as LAWS
Lines 255-262 of bend-kit-collections@0.1.4.1/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/LAWS.bend&start_line=255&end_line=262

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

# Ghost weight from tree shape: weight = stored size + 1, so OTip has weight 1 and
# OBin{lo, hi} has weight w(lo) + w(hi). Balance is Hirai-Yamamoto (delta 3, gamma 2).
def omap_weight(-K: Data, -V: Data, m: O.OMap<K, V>) -> Nat:
  match m:
    case O.OTip{}:
      1n
    case O.OBin{s, k, v, lo, hi}:
      Nat.add(omap_weight(K, V, lo), omap_weight(K, V, hi))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=OMap