BatchedMatmulPROOF.stretch_spec: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend as BatchedMatmulPROOF
Lines 343-356 of bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&start_line=343&end_line=356

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend as Batched

# The batch number of the build reads each operand's batch as the shape
# module broadcasts it.
# An index of a batch axis: the stretch of the build, the shape module's
# broadcast index.
def stretch_spec(+extent: Nat, +index: Nat) -> {Batched.stretch(index, Nat.is_eq(extent, 1n)) == Shape.broadcast_index(extent, index) : Nat}:
  match extent:
    case 0n:
      {==}
    case 1n+e:
      match e:
        case 0n:
          {==}
        case 1n+f:
          {==}

Uses (4):
  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_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=stretch