def rfold_append

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:443

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws
import bendtorch-core@0.1.0.0/src/tensor/contracts/replayed.bend as Replayed

443def rfold_append(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +accumulator: F32) ->
444  {rfold(shape, fill, ops, List.append(&2, Nat, xs, ys), accumulator) == rfold(shape, fill, ops, ys, rfold(shape, fill, ops, xs, accumulator)) : F32}:
445  match xs:
446    case Nil{}:
447      {==}
448    case +x <> +rest:
449      rfold_append(shape, fill, ops, rest, ys, F32.add(accumulator, Replayed.value(shape, fill, ops, U32.from_nat(x))))