ReduceParallelProof.table_walk: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 50-65 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=50&end_line=65

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as Fiber

# The index table of an aligned broadcast is walked as `Fiber.fiber_walk`
# says.
def table_walk(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>,
  +target: Nat, +below: {Nat.is_lt(target, Shape.numel(left)) == True{} : Bool}) ->
  Fiber.RestWalk(Shape.index_table(left, right, output), output, target, Shape.numel(output)):
  match alignment:
    case Shape.BAlign{+lp, +rp, minimal, +aligned}:
      +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left))
      +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right))
      Fiber.fiber_walk(Shape.pad(nl, left), Shape.pad(nr, right), output,
        %padding_left(left, right, output, lp, rp, aligned) : Shape.Aligned(Shape.pad(_, left), Shape.pad(nr, right), output)
        %padding_right(left, right, output, lp, rp, aligned) : Shape.Aligned(Shape.pad(lp, left), Shape.pad(_, right), output)
        aligned,
        target,
        %Equal.sym(Nat, Shape.numel(Shape.pad(nl, left)), Shape.numel(left), numel_pad(nl, left)) : {Nat.is_lt(target, _) == True{} : Bool}
        below)

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  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=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RestWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=fiber_walk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=numel_pad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=padding_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=padding_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad