def seek_bit

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/proofs/map_bridge.bend:97

import Base

97def seek_bit(-a: Quant, -V: Kind(a), lo: Map<a, V>, hi: Map<a, V>, p2: Nat, kb: String & Bool) -> Map<a, V> & String & Maybe<&2, String>:
98  (key2, b) = kb
99  match b:
100    case False{}:
101      Map.lo(a, V, String & Maybe<&2, String>, p2, hi, Map.seek(a, V, lo, key2))
102    case True{}:
103      Map.hi(a, V, String & Maybe<&2, String>, p2, lo, Map.seek(a, V, hi, key2))