def zero_fold

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

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
import bendtorch-core@0.1.0.0/src/tensor/dot_fold.bend as DotFold

596def zero_fold(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +row: U32, +column: U32,
597  values: List<&2, DotFold.Factors>, logical: Laws.LogicalDot(0n, left, right, a, b, row, column, 0n, values)) -> {DotFold.dot_fold(values, 0.0) == 0.0 : F32}:
598  match values:
599    case Nil{}:
600      {==}
601    case DotFold.Factors{lv, rv} <> rest:
602      Empty.absurd({DotFold.dot_fold(DotFold.Factors{lv, rv} <> rest, 0.0) == 0.0 : F32}, logical)