BackwardPROOF.somes_contribute: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 196-205 of bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&start_line=196&end_line=205

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

def somes_contribute(+node: Backward.Node, gradient: Maybe<&2, F32>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
  {Laws.somes(Backward.contribute(node, gradient, count, slots)) ==
    Laws.spread(node, Maybe.is_some(&2, F32, gradient), count, Laws.somes(slots)) : List<&2, Bool>}:
  match gradient:
    case None{}:
      {==}
    case Some{+value}:
      %vjp_targets(node, value) :
        {Laws.somes(Backward.deliver(Backward.vjp(node, value), count, slots)) == Laws.mark_all(_, count, Laws.somes(slots)) : List<&2, Bool>}
      somes_deliver(Backward.vjp(node, value), count, slots)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  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/backward.bend&name=Node
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=contribute
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=deliver
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=vjp
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=mark_all
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=somes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=spread
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=somes_deliver
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=vjp_targets