def w_pos

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

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

1220def w_pos(-K: Data, -V: Data, t: O.OMap<K, V>) -> Ord.LE(1n, W(K, V, t)):
1221  match t:
1222    case O.OTip{}:
1223      {==}
1224    case O.OBin{s, k, v, +lo, +hi}:
1225      pos_add(W(K, V, lo), W(K, V, hi), w_pos(K, V, lo))