law hmap_size_del_missing

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

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

661law hmap_size_del_missing:
662  for ~K: Data
663  for ~V: Data
664  for ~hash: K -> U32
665  for ~eq: K -> K -> Bool
666  for m: M.HMap<K, V>
667  for +k: K
668  for miss: {M.HMap.get(~K, ~V, ~hash, ~eq, m, k) == None{} : Maybe<&2, V>}
669  {M.HMap.size(K, V, M.HMap.del(~K, ~V, ~hash, ~eq, m, k))
670   == M.HMap.size(K, V, m) : Nat}