GatherLAWS.Added: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as GatherLAWS
Lines 274-284 of bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&start_line=274&end_line=284

import Base
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather

# The backward of input cell (o, i, r): from gradient cell (o, k, r) on, for
# `left` more k, a cell whose entry is i adds its word to the sum, in
# increasing k; a cell whose entry is another skips. `value` is the sum at
# the end.
def Added(+dg: Nat, -G: Array<F32>, +di: Nat, -I: Array<U32>, +kind: Gather.Lookup, +count: Nat, +inner: Nat, +o: Nat, +i: Nat, +r: Nat,
  left: Nat, +k: Nat, +acc: F32, +value: F32) -> Type:
  match left:
    case 0n:
      {value == acc : F32}
    case 1n+rest:
      AddStep<dg, G, di, I, kind, count, inner, o, i, r, rest, k, acc, value>

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather.bend&name=Lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend&name=AddStep