BackwardPROOF.somes_deliver: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 171-181 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=171&end_line=181

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_deliver(contributions: List<&2, Backward.Contribution>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
  {Laws.somes(Backward.deliver(contributions, count, slots)) ==
    Laws.mark_all(contribution_targets(contributions), count, Laws.somes(slots)) : List<&2, Bool>}:
  match contributions:
    case Nil{}:
      {==}
    case Con{Backward.Contribution{+target, +value}, rest}:
      %somes_bump(slots, count, target, value) :
        {Laws.somes(Backward.deliver(rest, count, Backward.bump(slots, count, target, value))) ==
          Laws.mark_all(contribution_targets(rest), count, _) : List<&2, Bool>}
      somes_deliver(rest, count, Backward.bump(slots, count, target, value))

Uses (12):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Contribution
  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=deliver
  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_PROOF.bend&name=contribution_targets
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=somes_bump