TensorChainPROOF.seeded_out: 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 507-542 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=507&end_line=542

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

def seeded_out(+node: Backward.Node, +shape: Shape.Shape, -value: Core.Dynamic, -saved: Backward.Saved, -slot: Gradient.Slot,
  -rest: List<&1, Backward.Entry>, +older: Nat, -ones: Core.Tensor<shape>, -copy: List<&1, Gradient.Slot>,
  made: {Core.new(shape, 1.0) == Done{ones} : Result<&2, &1, Core.Error, Core.Tensor<shape>>},
  same: {copy == Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older) : List<&1, Gradient.Slot>},
  out: Run<Backward.Entry{node, shape, value, saved, slot} <> rest, copy, 1n+older,
    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), Nil{}>) ->
  Passed<Backward.Entry{node, shape, value, saved, slot} <> rest, 1n+older, older, True{},
    Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older)>:
  match out:
    case Kept{done, gradients, swept, chained}:
      PassKept{done, gradients,
        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Done{gradients}),
          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Done{gradients}),
            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
            swept)),
        chained}
    case Stopped{done, error, swept}:
      PassStopped{done, error,
        Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Core.new(shape, 1.0)),
          Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}), (done, Fail{error}),
          Equal.cong(Result<&2, &1, Core.Error, Core.Tensor<shape>>, Backward.Swept(),
            made_ones => Backward.seeded(node, shape, value, saved, slot, rest, older, made_ones), Core.new(shape, 1.0), Done{ones}, made),
          Equal.trans(Backward.Swept(), Backward.seeded(node, shape, value, saved, slot, rest, older, Done{ones}),
            Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{copy}, 1n+older), (done, Fail{error}),
            Equal.cong(List<&1, Gradient.Slot>, Backward.Swept(),
              list => Backward.sweep(Backward.Entry{node, shape, value, saved, slot} <> rest, Done{list}, 1n+older),
              Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), copy,
              Equal.sym(List<&1, Gradient.Slot>, copy, Gradient.Held{Core.Packed{shape, ones}} <> Backward.unsets(older), same)),
            swept))}

Uses (23):
  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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=seeded
  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_backward.bend&name=unsets
  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/autograd/tensor_chain_PROOF.bend&name=Run
  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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new