def put_bit

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/map_bridge.bend:81

import Base

81def put_bit(-a: Quant, -V: Kind(a), x: V, p2: Nat, lo: Map<a, V>, hi: Map<a, V>, kb: String & Bool) -> Map<a, V>:
82  (key2, b) = kb
83  match b:
84    case False{}:
85      MNode{p2, Map.put(a, V, lo, key2, x), hi}
86    case True{}:
87      MNode{p2, lo, Map.put(a, V, hi, key2, x)}