English
An auxiliary step function for the cycle construction: given a current head and two lists, it yields the next head and updated lists by consuming the head of the second list if present, otherwise repeating the current head.
Русский
Вспомогательная функция шага для построения цикла: дано текущее значение и два списка, возвращается следующий элемент и обновленные списки, потребляя голову второго списка, если он непуст, иначе повторяя текущее значение.
LaTeX
$$$\\mathrm{cycleG}(v, l, v_0, l_0) = \\begin{cases} (v_0, l_0, v_0, l_0) & l = \\varnothing \\\\ (v_2, l_2, v_0, l_0) & l = (v_2, l_2) \\end{cases}$$$
Lean4
/-- An auxiliary definition for `Stream'.cycle` corecursive def -/
protected def cycleG : α × List α × α × List α → α × List α × α × List α
| (_, [], v₀, l₀) => (v₀, l₀, v₀, l₀)
| (_, List.cons v₂ l₂, v₀, l₀) => (v₂, l₂, v₀, l₀)
