def plan_left_right_rank

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/matmul.bend as Matrix

1172def plan_left_right_rank(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1173  -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1174  not_matrix: {Shape.rank_dimensions(Shape.dimensions(right)) != 2n : Nat}) ->
1175  {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1176  match dims:
1177    case Nil{}:
1178      {==}
1179    case +x <> Nil{}:
1180      {==}
1181    case +rows <> +inner <> Nil{}:
1182      plan_right_rank(left, right, rows, inner, Equal.sym(List<&2, U32>, [rows, inner], Shape.dimensions(left), same),
1183        Shape.dimensions(right), {==}, not_matrix)
1184    case +x <> +y <> +z <> +t:
1185      {==}