ReduceParallelProof.gather_append: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 120-126 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=120&end_line=126

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

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=add_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=word_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather