def h.edel_miss

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

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

2273def h.edel_miss(
2274  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, xs: List<&2, M.Entry<K, V>>, +k: K,
2275  miss: {M.HMap.entries.get(~K, ~V, ~eq, xs, k) == None{} : Maybe<&2, V>}
2276) -> {M.HMap.entries.del(~K, ~V, ~eq, xs, k) == xs : List<&2, M.Entry<K, V>>}:
2277  match xs:
2278    case Nil{}:
2279      {==}
2280    case Con{M.Entry{+key, +val}, +rest}:
2281      h.edel_miss.c(~K, ~V, ~eq, key, val, rest, k, eq(k, key), miss,
2282        e => h.edel_miss(~K, ~V, ~eq, rest, k, e))