def array_sum_keeps
bendtorch-core@0.1.0.0 · src/tensor/reduction.bend:130
import bendtorch-core@0.1.0.0/src/tensor/reduction.bend as Reduction
import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
130def array_sum_keeps(-depth: Nat, -original: Array<F32>, -balanced: Model.Balanced(F32, depth, original), fuel: Nat, +cursor: Nat,
131 -accumulator: F32, array: Array<F32>, -same: {array == original : Array<F32>}) ->
132 Fact<{Pair.snd(F32, Array<F32>, array_sum(fuel, cursor, accumulator, array)) == original : Array<F32>}>:
133 match fuel:
134 case 0n:
135 Fact{same}
136 case 1n+rest:
137 array_run_keeps(depth, original, balanced, rest, cursor, accumulator, array, Array.get(F32, array, U32.from_nat(cursor)), {==}, same)