BatchedMatmulPROOF.batch_part: 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 664-678 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=664&end_line=678

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

def batch_part(+rank: Nat, +o1: U32, +o2: U32, +first: Nat, +second: Nat,
  +e1: {U32.to_nat(o1) == first : Nat}, +e2: {U32.to_nat(o2) == second : Nat}) ->
  {Shape.naturals(Batched.batch_dims(rank, o1, o2)) == batch_nats(rank, first, second) : List<&2, Nat>}:
  match rank:
    case 0n:
      {==}
    case 1n+rest:
      match rest:
        case 0n:
          %Equal.sym(Nat, U32.to_nat(o2), second, e2) : {[_] == [second] : List<&2, Nat>}
          {==}
        case 1n+more:
          %Equal.sym(Nat, U32.to_nat(o1), first, e1) : {[_, U32.to_nat(o2)] == [first, second] : List<&2, Nat>}
          %Equal.sym(Nat, U32.to_nat(o2), second, e2) : {[first, _] == [first, second] : List<&2, Nat>}
          {==}

Uses (8):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=batch_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=batch_nats