English
corec' f produces a stream by repeatedly applying f to get a pair (β, α) from α and using the first component as the stream element.
Русский
corec' f строит поток, последовательно применяя f, чтобы получить пару (β, α) из α, и использовать первый элемент пары как элемент потока.
LaTeX
$$$\\text{corec'}\\,f = \\text{corec}(\\mathrm{fst} \\circ f)(\\mathrm{snd} \\circ f).$$$
Lean4
/-- Given a function `f : α → β × α`, `corec' f` creates a stream by repeatedly:
1. Starting with an initial value `a : α`
2. Applying `f` to get both the next stream element (β) and next state value (α)
This is a more convenient form when the next element and state are computed together. -/
def corec' (f : α → β × α) : α → Stream' β :=
corec (Prod.fst ∘ f) (Prod.snd ∘ f)
