BatchedMatmulPROOF.batch_nats: 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 643-653 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=643&end_line=653

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

# The plan's batch extents as naturals, as `Batched.batch_dims` lists them.
def batch_nats(+rank: Nat, +first: Nat, +second: Nat) -> List<&2, Nat>:
  match rank:
    case 0n:
      []
    case 1n+rest:
      match rest:
        case 0n:
          [second]
        case 1n+more:
          [first, second]

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat