TensorChainLAWS.gather: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as TensorChainLAWS
Lines 82-92 of bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&start_line=82&end_line=92

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

# Each slot of a newest-first list of count slots, the one with k older slots
# for id k, with what the log sends to it. A list longer than count keeps its
# slots past count, as the sweep does.
def gather(slots: List<&1, Gradient.Slot>, +count: Nat, log: Log()) -> Slots():
  match slots count:
    case Nil{} count:
      Done{Nil{}}
    case Con{slot, rest} 0n:
      Done{slot <> rest}
    case Con{slot, rest} 1n+below:
      gather_step(take(log, below, slot), more => gather(rest, below, more))

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=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_chain_LAWS.bend&name=Log
  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=gather_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=take