def zero_cell

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

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

607def zero_cell(+left: Shape.Shape, +right: Shape.Shape, -a: Core.Tensor<left>, -b: Core.Tensor<right>, +output: Shape.Shape,
608  -out: Core.Tensor<output>, +position: Nat, cell: Laws.ProductCell<0, left, right, a, b, output, out, position>) -> ZeroCell<output, out, position>:
609  Laws.ProductCell{row, column, coordinate, decoded, coordinates, word_exact, factors, logical, value, fold, checked, observed} = cell
610  ZeroCell{Equal.trans(Maybe<&2, F32>, Core.checked_observe(output, out, U32.from_nat(position)), Some{value}, Some{0.0}, observed,
611    Equal.cong(F32, Maybe<&2, F32>, x => Some{x}, value, 0.0,
612      Equal.trans(F32, value, DotFold.dot_fold(factors, 0.0), 0.0, fold, zero_fold(left, right, a, b, row, column, factors, logical))))}