def h.elen_del_hit

bend-kit-collections@0.1.4.1 · PROOF.bend:2248

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

2248def h.elen_del_hit(
2249  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry<K, V>>, +k: K, -w: V,
2250  hit: {M.HMap.entries.get(~K, ~V, ~eq, xs, k) == Some{w} : Maybe<&2, V>}
2251) -> {1n+h.len(K, V, M.HMap.entries.del(~K, ~V, ~eq, xs, k)) == h.len(K, V, xs) : Nat}:
2252  match xs:
2253    case Nil{}:
2254      h.none_some({1n == 0n : Nat}, V, w, hit)
2255    case Con{M.Entry{+key, +val}, +rest}:
2256      h.elen_del_hit.c(~K, ~V, ~eq, key, val, rest, k, w, eq(k, key), hit,
2257        e => h.elen_del_hit(~K, ~V, ~eq, rest, k, w, e))