Map.ins.go: def of Base
Import: import Base
Lines 2776-2797 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=2776&end_line=2797

import Base

# t says whether the key splits deeper than node: else it goes above
def Map.ins.go(
  -a: Quant, -V: Kind(a), node: Map<a, V>, x: V, +p: Nat, kb: String & Bool,
  t: Bool
) -> Map<a, V>:
  match node kb t:
    case MNode{q, lo, hi} Tuple{key, b} False{}:
      Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi})
    case MNode{q, MTip{}, hi} Tuple{key, False{}} True{}:
      MNode{q, MLeaf{key, x}, hi}
    case MNode{q, MLeaf{k, v}, hi} Tuple{key, False{}} True{}:
      MNode{q, Map.ins.splice(a, V, p, key, x, MLeaf{k, v}), hi}
    case MNode{q, MNode{+r, c, d}, hi} Tuple{key, False{}} True{}:
      MNode{q, Map.ins.go(a, V, MNode{r, c, d}, x, p, Map.bit(key, r), Nat.is_lt(r, p)), hi}
    case MNode{q, lo, MTip{}} Tuple{key, True{}} True{}:
      MNode{q, lo, MLeaf{key, x}}
    case MNode{q, lo, MLeaf{k, v}} Tuple{key, True{}} True{}:
      MNode{q, lo, Map.ins.splice(a, V, p, key, x, MLeaf{k, v})}
    case MNode{q, lo, MNode{+r, c, d}} Tuple{key, True{}} True{}:
      MNode{q, lo, Map.ins.go(a, V, MNode{r, c, d}, x, p, Map.bit(key, r), Nat.is_lt(r, p))}
    case m _ _:
      m

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map.bit
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map.ins.splice
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String