def rank_clash

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:1070

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

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