def somes_deliver

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:171

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

171def somes_deliver(contributions: List<&2, Backward.Contribution>, +count: Nat, +slots: List<&2, Maybe<&2, F32>>) ->
172  {Laws.somes(Backward.deliver(contributions, count, slots)) ==
173    Laws.mark_all(contribution_targets(contributions), count, Laws.somes(slots)) : List<&2, Bool>}:
174  match contributions:
175    case Nil{}:
176      {==}
177    case Con{Backward.Contribution{+target, +value}, rest}:
178      %somes_bump(slots, count, target, value) :
179        {Laws.somes(Backward.deliver(rest, count, Backward.bump(slots, count, target, value))) ==
180          Laws.mark_all(contribution_targets(rest), count, _) : List<&2, Bool>}
181      somes_deliver(rest, count, Backward.bump(slots, count, target, value))