Chacha8rand.stream_go: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8rand
Lines 194-203 of bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&start_line=194&end_line=203

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W

# n outputs: the words left of the current iteration, then the next
# iterations, each keyed by the last 32 bytes of the one before
def stream_go(n: Nat, buf: List<&2, W.U64>, +key: List<&2, U32>) -> List<&2, W.U64>:
  match n buf:
    case 0n _:
      []
    case 1n+p Con{x, rest}:
      Con{x, stream_go(p, rest, key)}
    case 1n+p Nil{}:
      Con{head(words64(output(key))), stream_go(p, tail(words64(output(key))), next_key(key))}

Uses (9):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=next_key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend&name=words64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64