BatchedMatmulPROOF.geometry_shaped: 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 729-753 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=729&end_line=753

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
import bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend as Laws

def geometry_shaped(+lr: Nat, +l1: U32, +l2: U32, +rows: U32, +inner: U32, +lv: Bool, +rr: Nat, +r1: U32, +r2: U32, +columns: U32,
  +rinner: U32, +rv: Bool, +o1: U32, +o2: U32, +same: {U32.to_nat(inner) == U32.to_nat(rinner) : Nat},
  +e1: {U32.to_nat(o1) == Laws.extent(U32.to_nat(l1), U32.to_nat(r1)) : Nat},
  +e2: {U32.to_nat(o2) == Laws.extent(U32.to_nat(l2), U32.to_nat(r2)) : Nat},
  result: Shape.ConstructResult<List.append(&2, U32, Batched.batch_dims(Batched.larger(lr, rr), o1, o2), Batched.matrix_dims(rows, lv, columns, rv))>) ->
  ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
    Batched.planned_shape(Batched.batch_dims(Batched.larger(lr, rr), o1, o2), rows, inner, columns, l1, l2, r1, r2, o1, o2, lv, rv,
      List.append(&2, U32, Batched.batch_dims(Batched.larger(lr, rr), o1, o2), Batched.matrix_dims(rows, lv, columns, rv)), result)):
  match result:
    case Shape.SError{error}:
      Unit{}
    case Shape.SBuilt{+shape, +preserved}:
      Laws.Geometry{
        Equal.trans(List<&2, Nat>, Shape.naturals(Shape.dimensions(shape)),
          Shape.naturals(List.append(&2, U32, Batched.batch_dims(Batched.larger(lr, rr), o1, o2), Batched.matrix_dims(rows, lv, columns, rv))),
          List.append(&2, Nat, batch_nats(Batched.larger(lr, rr), Laws.extent(U32.to_nat(l1), U32.to_nat(r1)), Laws.extent(U32.to_nat(l2), U32.to_nat(r2))),
            List.append(&2, Nat, Laws.kept(lv, U32.to_nat(rows)), Laws.kept(rv, U32.to_nat(columns)))),
          Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(shape),
            List.append(&2, U32, Batched.batch_dims(Batched.larger(lr, rr), o1, o2), Batched.matrix_dims(rows, lv, columns, rv)), preserved),
          output_nats(Batched.larger(lr, rr), o1, o2, Laws.extent(U32.to_nat(l1), U32.to_nat(r1)), Laws.extent(U32.to_nat(l2), U32.to_nat(r2)),
            e1, e2, rows, lv, columns, rv)),
        {==},
        Equal.cong(Nat, List<&2, Nat>, x => [U32.to_nat(r1), U32.to_nat(r2), x, U32.to_nat(columns)], U32.to_nat(inner), U32.to_nat(rinner), same),
        pair_nats(U32.to_nat(o1), U32.to_nat(o2), Laws.extent(U32.to_nat(l1), U32.to_nat(r1)), Laws.extent(U32.to_nat(l2), U32.to_nat(r2)), e1, e2),
        {==}}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=ConstructResult
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  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.bend&name=larger
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=matrix_dims
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul.bend&name=planned_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=Geometry
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=extent
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_LAWS.bend&name=kept
  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=batch_nats
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=output_nats
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/batched_matmul_PROOF.bend&name=pair_nats