law omap_get_put_other_key

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

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

207law omap_get_put_other_key:
208  for ~K: Data
209  for ~V: Data
210  for ~cmp: K -> K -> Cmp
211  for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
212  for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
213  for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
214  for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
215  for m: O.OMap<K, V>
216  for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
217  for +k2: K
218  for +k: K
219  for ne: {cmp(k2, k) != EQ{} : Cmp}
220  for +v: V
221  {O.OMap.get(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k2, v), k)
222   == O.OMap.get(~K, ~V, ~cmp, m, k) : Maybe<&2, V>}