law hmap_size_put_replace

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

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

636law hmap_size_put_replace:
637  for ~K: Data
638  for ~V: Data
639  for ~hash: K -> U32
640  for ~eq: K -> K -> Bool
641  for m: M.HMap<K, V>
642  for +k: K
643  for +v: V
644  for -w: V
645  for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>}
646  {M.HMap.size(K, V, M.HMap.put(~K, ~V, ~hash, ~eq, m, k, v))
647   == M.HMap.size(K, V, m) : Nat}