def left_extents
bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1368
import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
1368def left_extents(+left: Shape.Shape, +rows: U32, +inner: U32, +le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}) ->
1369 {Shape.extents(left) == [U32.to_nat(rows), U32.to_nat(inner)] : List<&2, Nat>}:
1370 Equal.cong(List<&2, U32>, List<&2, Nat>, dims => Shape.naturals(dims), Shape.dimensions(left), [rows, inner], le)