def restarted

bendtorch-core@0.1.0.0 · src/autograd/tensor_chain_PROOF.bend:50

import Base
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient

50def restarted(x: Gradient.Slot, -rest: List<&1, Gradient.Slot>, +below: Nat, out: Started<rest, below>) ->
51  Started<x <> rest, 1n+below>:
52  Started{copy, same, pulls} = out
53  Started{x <> copy, Equal.cong(List<&1, Gradient.Slot>, List<&1, Gradient.Slot>, more => x <> more, copy, rest, same),
54    Cell{x, rest, Nil{}, {==}, {==}, pulls}}