def h.gd_same.lf

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

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

3227# get after del.
3228def h.gd_same.lf(
3229  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +o: U32,
3230  +es: List<&2, M.Entry<K, V>>, +hk: U32, +k: K, b: Bool, eb: {b == U32.is_eq(o, hk) : Bool},
3231  ed: {h.EG(~K, ~V, ~eq, M.HMap.entries.del(~K, ~V, ~eq, es, k), k) == None{} : Maybe<&2, V>}
3232) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.dl(~K, ~V, ~eq, b, o, es, k), hk, k) == None{} : Maybe<&2, V>}:
3233  match b:
3234    case True{}:
3235      %h.get_leaf(~K, ~V, ~eq, 1n+p, mask, o, M.HMap.entries.del(~K, ~V, ~eq, es, k), hk, k) : {_ == None{} : Maybe<&2, V>}
3236      h.bool_none(V, U32.is_eq(o, hk), h.EG(~K, ~V, ~eq, M.HMap.entries.del(~K, ~V, ~eq, es, k), k), ed)
3237    case False{}:
3238      %eb : {M.HMap.bool(Maybe<&2, V>, _, u => h.EG(~K, ~V, ~eq, es, k), u => None{}) == None{} : Maybe<&2, V>}
3239      {==}