MatmulPROOF.prefix_cell_case: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 329-339 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=329&end_line=339

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend as Laws

def prefix_cell_case(+inner: U32, +left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
  +output: Shape.Shape, -out: Core.Tensor<output>, +cursor: Nat, +position: Nat,
  current: Laws.ProductCell<inner, left, right, a, b, output, out, cursor>,
  prior: @+position: Nat -> @earlier: {Nat.is_lt(position, cursor) == True{} : Bool} -> Laws.ProductCell<inner, left, right, a, b, output, out, position>,
  split: Either<&2, &2, {Nat.is_lt(position, cursor) == True{} : Bool}, {position == cursor : Nat}>) -> Laws.ProductCell<inner, left, right, a, b, output, out, position>:
  match split:
    case Inl{earlier}:
      prior(position, earlier)
    case Inr{equal}:
      %Equal.sym(Nat, position, cursor, equal) : Laws.ProductCell<inner, left, right, a, b, output, out, _>
      current

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_LAWS.bend&name=ProductCell