def plan_left_rank

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

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

1135def plan_left_rank(+left: Shape.Shape, +right: Shape.Shape, +dims: List<&2, U32>,
1136  -same: {dims == Shape.dimensions(left) : List<&2, U32>},
1137  not_matrix: {Shape.rank_dimensions(dims) != 2n : Nat}) ->
1138  {Matrix.plan_left(left, right, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1139  match dims:
1140    case Nil{}:
1141      {==}
1142    case +x <> Nil{}:
1143      {==}
1144    case +rows <> +inner <> Nil{}:
1145      Empty.absurd({Matrix.plan_left(left, right, [rows, inner], same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1146        not_matrix({==}))
1147    case +x <> +y <> +z <> +t:
1148      {==}