def gather_append

bendtorch-core@0.1.0.0 · src/autograd/reduce_parallel_proof.bend:120

import Base
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

120def gather_append(+values: List<&2, F32>, +xs: List<&2, Nat>, +ys: List<&2, Nat>, +total: Maybe<&2, F32>) ->
121  {gather(values, List.append(&2, Nat, xs, ys), total) == gather(values, ys, gather(values, xs, total)) : Maybe<&2, F32>}:
122  match xs:
123    case Nil{}:
124      {==}
125    case +x <> +rest:
126      gather_append(values, rest, ys, ReduceLaws.add_word(total, ReduceLaws.word_at(values, x)))