def h.r_none

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

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

3036def h.r_none(
3037  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool, +o: U32,
3038  +es: List<&2, M.Entry<K, V>>, +k: K, ne: {U32.is_eq(o, hash(k)) == False{} : Bool}
3039) -> {None{} == h.R(~K, ~V, ~hash, ~eq, o, es, k) : Maybe<&2, V>}:
3040  %h.sb(U32.is_eq(o, hash(k)), False{}, ne)
3041    : {None{} == M.HMap.bool(Maybe<&2, V>, _, u => h.EG(~K, ~V, ~eq, es, k), u => None{}) : Maybe<&2, V>}
3042  {==}