def bif.w

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

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

1524def bif.w(
1525  -K: Data, -V: Data, heavy_hi: Bool, heavy_lo: Bool, -k: K, -v: V,
1526  +lo: O.OMap<K, V>, +hi: O.OMap<K, V>
1527) -> {Nat.add(W(K, V, lo), W(K, V, hi))
1528      == W(K, V, Laws.g_balance.if(K, V, heavy_hi, heavy_lo, k, v, lo, hi)) : Nat}:
1529  match heavy_hi heavy_lo:
1530    case True{} _:
1531      rl.w(K, V, hi, k, v, lo)
1532    case False{} True{}:
1533      rh.w(K, V, lo, k, v, hi)
1534    case False{} False{}:
1535      {==}