TensorChainPROOF.started_pulls: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
Lines 458-462 of bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&start_line=458&end_line=462

import Base
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as Laws

def started_pulls(entries: List<&1, Backward.Entry>, -gradients: List<&1, Gradient.Slot>, +count: Nat, -gs: List<&1, Gradient.Slot>,
  succeeded: {Laws.result(Backward.sweep(entries, Done{gradients}, count)) == Done{gs} : Laws.Slots()}, init: Started<gradients, count>) ->
  {Laws.chained(entries, gradients, count, Nil{}) == Done{gs} : Laws.Slots()}:
  Started{copy, same, pulls} = init
  conclude(entries, copy, gradients, count, gs, same, succeeded, swept_pulls(entries, Done{copy}, gradients, count, Nil{}, pulls))

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/gradient.bend&name=Slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Entry
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=sweep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=Slots
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=chained
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=Started
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=conclude
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=swept_pulls