BatchedMatmulPROOF.geometry_decided: 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 770-785 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=770&end_line=785

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

def geometry_decided(+lr: Nat, +l1: U32, +l2: U32, +rows: U32, +inner: U32, +lv: Bool, +rr: Nat, +r1: U32, +r2: U32, +columns: U32,
  +rinner: U32, +rv: Bool, decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner))>) ->
  ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
    Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv},
      Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner)))):
  match decision:
    case Shape.BFalse{equal}:
      %equal : ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
        Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv}, _))
      Unit{}
    case Shape.BTrue{+equal}:
      %equal : ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
        Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv}, _))
      geometry_batched(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
        Lifecycle.natural_equal(U32.to_nat(inner), U32.to_nat(rinner), equal),
        Batched.axis(l1, r1), Batched.axis(l2, r2), axis_meaning(l1, r1), axis_meaning(l2, r2))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=Batch
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=Operand
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=axis
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=compatible
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=ExpectedOf
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=axis_meaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=geometry_batched
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend&name=natural_equal