English
Let s be a weak sequence. For every natural number n, collect(s, n) yields the first n outputs produced by s; in particular, collect(s, n) equals the prefix of length n of the produced sequence, i.e., collect(s, n) = List.take(n, toList(s)).
Русский
Пусть s — слабая последовательность. Для каждого натурального числа n функция collect(s, n) возвращает первые n элементов, порождаемых s; то есть collect(s, n) равняется префиксу длины n полученной последовательности: collect(s, n) = List.take(n, toList(s)).
LaTeX
$$$$ \forall s:\mathrm{WSeq}\ \alpha,\ \forall n:\mathbb{N},\ \text{collect}(s,n)=\text{List.take}(n,\text{toList}(s)). $$$$
Lean4
/-- Like take, but does not wait for a result. Calculates `n` steps of
computation and returns the sequence computed so far -/
def collect (s : WSeq α) (n : ℕ) : List α :=
(Seq.take n s).filterMap id
