~/jendhub

def omap_weight

bend-kit-collections@0.1.4.1 · LAWS.bend:255

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

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

Uses (3)

Used by (6)