English
Let f: β → Option(α × β). The corecursor corec f b constructs a Seq α by the rule: if f(b) = none then corec f b = nil; if f(b) = some (a, s) then corec f b = cons a (corec f s).
Русский
Пусть f: β → Option(α × β). Ядроиндекс corec f b строит последовательность Seq α так: если f(b) = none, тогда corec f b = nil; если f(b) = some (a, s), тогда corec f b = cons a (corec f s).
LaTeX
$$$\\text{corec}(f)(b) = \\begin{cases} \\mathrm{nil}, & \\text{если } f(b) = \\mathrm{none}, \\\\ \\mathrm{cons}(a, \\text{corec}(f)(s)), & \\text{если } f(b) = \\mathrm{some}(a, s). \\end{cases}$$$
Lean4
/-- Corecursor over pairs of `Option` values -/
def f (f : β → Option (α × β)) : Option β → Option α × Option β
| none => (none, none)
| some b =>
match f b with
| none => (none, none)
| some (a, b') => (some a, some b')
