BatchedMatmul.left_start: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as BatchedMatmul
Lines 260-267 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&start_line=260&end_line=267

import Base
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix

# The first term's offsets of cell `position`: batch b = position / (rows *
# columns) splits into (b / o2, b % o2), and each operand reads its own
# batch, a stretched axis at 0, then the cell's row and column at term 0.
def left_start(+layout: Layout, +position: Nat) -> Nat:
  Layout{+lo, ro, +inner, +rows, +columns, +l1, +l2, r1, r2, +o2} = layout
  +batch = Nat.div(position, Nat.mul(rows, columns))
  Nat.add(Nat.mul(batch_number(l1, l2, Nat.div(batch, o2), Nat.mod(batch, o2)), Nat.mul(rows, inner)),
    Matrix.read_offset(lo, inner, rows, Nat.div(Nat.mod(position, Nat.mul(rows, columns)), columns), 0n))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=Layout
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=batch_number
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul.bend&name=read_offset