law omap_get_put_same

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

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

193law omap_get_put_same:
194  for ~K: Data
195  for ~V: Data
196  for ~cmp: K -> K -> Cmp
197  for ~refl: @x: K -> {cmp(x, x) == EQ{} : Cmp}
198  for ~eq: @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K}
199  for ~flip: @x: K -> @y: K -> {cmp(y, x) == flip(cmp(x, y)) : Cmp}
200  for ~trans: @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp}
201  for m: O.OMap<K, V>
202  for tree: {searchtree(~K, ~V, ~cmp, m) == True{} : Bool}
203  for +k: K
204  for +v: V
205  {O.OMap.get(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, m, k, v), k) == Some{v} : Maybe<&2, V>}