def geometry_ops

bendtorch-core@0.1.0.0 · src/tensor/batched_matmul_PROOF.bend:787

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

787def geometry_ops(+lr: Nat, +l1: U32, +l2: U32, +rows: U32, +inner: U32, +lv: Bool, +rr: Nat, +r1: U32, +r2: U32, +columns: U32,
788  +rinner: U32, +rv: Bool) ->
789  ExpectedOf(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv,
790    Batched.compatible(Batched.Operand{Batched.Batch{lr, l1, l2}, rows, inner, lv}, Batched.Operand{Batched.Batch{rr, r1, r2}, columns, rinner, rv},
791      Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner)))):
792  geometry_decided(lr, l1, l2, rows, inner, lv, rr, r1, r2, columns, rinner, rv, Shape.bool_case(Nat.is_eq(U32.to_nat(inner), U32.to_nat(rinner))))