TensorChainPROOF.newer_step: 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 555-571 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=555&end_line=571

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
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 newer_step(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
  -rest: List<&1, Backward.Entry>, -below: Nat, +older: Nat, -slots: List<&1, Gradient.Slot>,
  out: Passed<rest, below, older, Backward.at_head(below, older), slots>) ->
  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+below, older, False{}, Gradient.Unset{} <> slots>:
  match out:
    case PassKept{done, gradients, passed, chained}:
      PassKept{Backward.Entry{node, shape, value, saved, slot} <> done, Gradient.Unset{} <> gradients,
        Equal.cong(Backward.Swept(), Backward.Swept(),
          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Done{gradients}), passed),
        Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, Gradient.Unset{}, result),
          Laws.chained(rest, slots, below, Nil{}), Done{gradients}, chained)}
    case PassStopped{done, error, passed}:
      PassStopped{Backward.Entry{node, shape, value, saved, slot} <> done, error,
        Equal.cong(Backward.Swept(), Backward.Swept(),
          pair => Backward.finished(Backward.Entry{node, shape, value, saved, slot}, Gradient.Unset{}, pair),
          Backward.pass(rest, below, older, Backward.at_head(below, older)), (done, Fail{error}), passed)}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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/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=Node
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=Saved
  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=at_head
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=finished
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=pass
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=prepend
  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_PROOF.bend&name=Passed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic