type ProductPrefix

bendtorch-core@0.1.0.0 · src/tensor/matmul_LAWS.bend:71

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

71type ProductPrefix<-inner: U32, -left: Shape.Shape, -right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>,
72  -output: Shape.Shape, -ra: Core.Tensor<left>, -rb: Core.Tensor<right>, -out: Core.Tensor<output>, -cursor: Nat> is Data:
73  ProductPrefix{-left_kept: @+other: U32 -> {Core.checked_observe(left, ra, other) == Core.checked_observe(left, a, other) : Maybe<&2, F32>},
74    -right_kept: @+other: U32 -> {Core.checked_observe(right, rb, other) == Core.checked_observe(right, b, other) : Maybe<&2, F32>},
75    -cells: @+position: Nat -> @earlier: {Nat.is_lt(position, cursor) == True{} : Bool} -> ProductCell<inner, left, right, a, b, output, out, position>}