English
Generalized corecursor for Cofix F allowing the return of a fully formed value instead of an immediate recursive call.
Русский
Обобщённый коркурсор Cofix F, позволяющий вернуть полностью сформированное значение вместо немедленного рекурсивного вызова.
LaTeX
$$$\\mathrm{corec'}\\ g\\ x : \\mathrm{Cofix}\\,F\\,\\alpha \\\\equiv\\; \\mathrm{Cofix.corec}\\; (\\lambda X. g\\; (Cofix.dest)\\; X)\\; x.$$$
Lean4
/-- More flexible corecursor for `Cofix F`. Allows the return of a fully formed
value instead of making a recursive call -/
def corec' {α : TypeVec n} {β : Type u} (g : β → F (α.append1 (Cofix F α ⊕ β))) (x : β) : Cofix F α :=
let f : (α ::: Cofix F α) ⟹ (α ::: (Cofix F α ⊕ β)) := id ::: Sum.inl
Cofix.corec (Sum.elim (MvFunctor.map f ∘ Cofix.dest) g) (Sum.inr x : Cofix F α ⊕ β)
