English
A refined corecursor that, for a functor F, allows forming a value either immediately or via recursive steps, encoding a choice between a finished value and a recursively produced one.
Русский
Улучшенный корекурсор, для функторa F, позволяет получить значение либо сразу, либо через рекурсивные шаги, кодируя выбор между готовым значением и рекурсивно порождаемым.
LaTeX
$$$corec' : (F \text{ with } X) \to (α \to M P) \to α \to M P$ (определение)
$$
Lean4
/-- corecursor where it is possible to return a fully formed value at any point
of the computation -/
def corec' {α : Type u} (F : ∀ {X : Type (max u uA uB)}, (α → X) → α → M P ⊕ P X) (x : α) : M P :=
corec₁
(fun _ rec (a : M P ⊕ α) =>
let y := Sum.bind a (F (rec ∘ Sum.inr))
match y with
| Sum.inr y => y
| Sum.inl y => P.map (rec ∘ Sum.inl) (M.dest y))
(@Sum.inr (M P) _ x)
