def h.eg_put_same.c

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

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

2087def h.eg_put_same.c(
2088  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +key: K, +val: V,
2089  +rest: List<&2, M.Entry<K, V>>, +k: K, +v: V, b: Bool, eb: {b == eq(k, key) : Bool},
2090  ih: {M.HMap.entries.get(~K, ~V, ~eq, M.HMap.entries.put(~K, ~V, ~eq, rest, k, v), k) == Some{v} : Maybe<&2, V>}
2091) -> {M.HMap.entries.get(~K, ~V, ~eq, h.epc(~K, ~V, ~eq, b, key, val, rest, k, v), k) == Some{v} : Maybe<&2, V>}:
2092  match b:
2093    case True{}:
2094      %eb : {h.egc(~K, ~V, ~eq, _, v, rest, k) == Some{v} : Maybe<&2, V>}
2095      {==}
2096    case False{}:
2097      %eb : {h.egc(~K, ~V, ~eq, _, val, M.HMap.entries.put(~K, ~V, ~eq, rest, k, v), k) == Some{v} : Maybe<&2, V>}
2098      ih