law hmap_size_del

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

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

649law hmap_size_del:
650  for ~K: Data
651  for ~V: Data
652  for ~hash: K -> U32
653  for ~eq: K -> K -> Bool
654  for m: M.HMap<K, V>
655  for +k: K
656  for -w: V
657  for hit: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == Some{w} : Maybe<&2, V>}
658  {1n+M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k))
659   == M.HMap.size(K, V, m) : Nat}