TensorChainPROOF.Stop: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
Lines 195-198 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=195&end_line=198

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

# What a sweep from a push-side state does, with the pull side's answer when
# it succeeds: done and gradients are the sweep's own outputs.
type Stop<-entries: List<&1, Backward.Entry>, -error: Backward.Error, -count: Nat> is Data:
  Stop{-done: List<&1, Backward.Entry>, swept: {Backward.sweep(entries, Fail{error}, count) == (done, Fail{error}) : Backward.Swept()}}

Uses (8):
  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=Base/base.bend&name=Sigma
  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=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Swept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=sweep