BackwardLAWS.bump_target: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as BackwardLAWS
Lines 295-304 of bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&start_line=295&end_line=304

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward

# A contribution to node target reaches exactly the slot of that node and no
# other, for any list of slots.
law bump_target:
  for +newer: List<&2, Maybe<&2, F32>>
  for +slot: Maybe<&2, F32>
  for +rest: List<&2, Maybe<&2, F32>>
  for +value: F32
  {Backward.bump(List.append(&2, Maybe<&2, F32>, newer, slot <> rest),
      List.length(&2, Maybe<&2, F32>, List.append(&2, Maybe<&2, F32>, newer, slot <> rest)), List.length(&2, Maybe<&2, F32>, rest), value) ==
    List.append(&2, Maybe<&2, F32>, newer, Backward.accumulate(slot, Some{value}) <> rest) : List<&2, Maybe<&2, F32>>}

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=accumulate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bump
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=bumped
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=append_ne
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=eq_refl