def h.edel_miss.c

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

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

2259def h.edel_miss.c(
2260  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +key: K, +val: V,
2261  +rest: List<&2, M.Entry<K, V>>, +k: K, b: Bool,
2262  miss: {h.egc(~K, ~V, ~eq, b, val, rest, k) == None{} : Maybe<&2, V>},
2263  ih: {M.HMap.entries.get(~K, ~V, ~eq, rest, k) == None{} : Maybe<&2, V>}
2264    -> {M.HMap.entries.del(~K, ~V, ~eq, rest, k) == rest : List<&2, M.Entry<K, V>>}
2265) -> {h.edc(~K, ~V, ~eq, b, key, val, rest, k) == M.Entry{key, val} <> rest : List<&2, M.Entry<K, V>>}:
2266  match b:
2267    case True{}:
2268      h.some_none({rest == M.Entry{key, val} <> rest : List<&2, M.Entry<K, V>>}, V, val, miss)
2269    case False{}:
2270      Equal.cong(List<&2, M.Entry<K, V>>, List<&2, M.Entry<K, V>>, t => M.Entry{key, val} <> t,
2271        M.HMap.entries.del(~K, ~V, ~eq, rest, k), rest, ih(miss))