def sequential_snoc

bendtorch-core@0.1.0.0 · src/tensor/contracts/sum_proof.bend:16

import Base
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction

16def sequential_snoc(+values: List<&2, F32>, +word: F32, +accumulator: F32) ->
17  {Reduction.sequential_sum(List.append(&2, F32, values, [word]), accumulator) ==
18    F32.add(Reduction.sequential_sum(values, accumulator), word) : F32}:
19  match values:
20    case Nil{}:
21      {==}
22    case +value <> +rest:
23      sequential_snoc(rest, word, F32.add(accumulator, value))