def prefix_cell_case

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

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

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