Array.map.at: def of Base
Import: import Base
Lines 2627-2632 of Base/base.bend: https://jend.leeeet.dev/read.txt?path=Base/base.bend&start_line=2627&end_line=2632

import Base

def Array.map.at(
  ~T: Data, ~U: Data, ~f: T -> U, v: U, an: Array<T> & U32
) -> Array<U>:
  (a, +n) = an
  Array.map.go(~T, ~U, ~f, U32.to_nat(U32.sub(n, 1)), 1,
    Array.new(U, U32.log2(n), v), Array.get(T, a, 1))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.map.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.new
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.log2
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat