def plan_right_rank

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

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

1156def plan_right_rank(-left: Shape.Shape, +right: Shape.Shape, +rows: U32, +inner: U32,
1157  -le: {Shape.dimensions(left) == [rows, inner] : List<&2, U32>}, +dims: List<&2, U32>,
1158  -same: {dims == Shape.dimensions(right) : List<&2, U32>},
1159  not_matrix: {Shape.rank_dimensions(dims) != 2n : Nat}) ->
1160  {Matrix.plan_right(left, right, rows, inner, le, dims, same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>}:
1161  match dims:
1162    case Nil{}:
1163      {==}
1164    case +x <> Nil{}:
1165      {==}
1166    case +right_inner <> +columns <> Nil{}:
1167      Empty.absurd({Matrix.plan_right(left, right, rows, inner, le, [right_inner, columns], same) == Fail{Matrix.RankMismatch{}} : Result<&2, &2, Matrix.Error, Matrix.Plan<left, right>>},
1168        not_matrix({==}))
1169    case +x <> +y <> +z <> +t:
1170      {==}