BendMlTensor.Mat.reshape: def of bend-ml-tensor@0.1.2.0
Import: import bend-ml-tensor@0.1.2.0/main.bend as BendMlTensor
Lines 302-306 of bend-ml-tensor@0.1.2.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-tensor@0.1.2.0/main.bend&start_line=302&end_line=306

import Base

# Reshape: compiles only with the PROOF that the number of elements does not change.
def Mat.reshape(-r1: Nat, -c1: Nat, r2: Nat, +c2: Nat, -p: {Nat.mul(r1, c1) == Nat.mul(r2, c2) : Nat}, a: Mat<r1, c1>) -> Mat<r2, c2>:
  match a:
    case Mat{x}:
      Mat{chunk.l(r2, c2, flatten.l(x))}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=Mat
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=chunk.l
  https://jend.leeeet.dev/definition.txt?path=bend-ml-tensor@0.1.2.0/main.bend&name=flatten.l