def h.fresh_get

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

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

2888# get after put, same key.
2889def h.fresh_get(
2890  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, ~refl: @x: K -> {eq(x, x) == True{} : Bool},
2891  p: Nat, +mm: U32, +hk: U32, +k: K, +v: V
2892) -> {h.G(~K, ~V, ~eq, p, mm, M.HLeaf{hk, [M.Entry{k, v}]}, hk, k) == Some{v} : Maybe<&2, V>}:
2893  match p:
2894    case 0n:
2895      h.eg_put_same(~K, ~V, ~eq, ~refl, Nil{}, k, v)
2896    case 1n+q:
2897      %h.g_lf_t(~K, ~V, ~eq, q, mm, hk, [M.Entry{k, v}], hk, k, h.u_refl(hk)) : {_ == Some{v} : Maybe<&2, V>}
2898      h.eg_put_same(~K, ~V, ~eq, ~refl, Nil{}, k, v)