MatmulPROOF.rank_clash: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 1070-1078 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=1070&end_line=1078

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def rank_clash(+left: Shape.Shape, +right: Shape.Shape, +dimensions: List<&2, U32>,
  +same: {dimensions == Shape.dimensions(left) : List<&2, U32>}, +different: {Nat.is_eq(Shape.rank_dimensions(dimensions), 2n) == False{} : Bool},
  -valid: Totality.MatrixInputs<left, right>) -> Totality.Impossible:
  Totality.Impossible{{\{Totality.MatrixInputs: rows => inner => right_inner => columns => le => re => compatible => supported =>
    Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), True{},
      Equal.sym(Bool, Nat.is_eq(Shape.rank_dimensions(dimensions), 2n), False{}, different),
      Equal.cong(List<&2, U32>, Bool, values => Nat.is_eq(Shape.rank_dimensions(values), 2n), dimensions, [rows, inner],
        Equal.trans(List<&2, U32>, dimensions, Shape.dimensions(left), [rows, inner], same, le))))} :
          Totality.MatrixInputs<left, right> -> Empty}(valid)}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  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.sym
  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=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  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=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=Impossible
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=MatrixInputs