corec₁ — Mathlib

English

Corecursor for Cofix F. The shape allows recursive calls to look like recursive calls.

Русский

Корекурс Cofix F. Шаблон позволяет, чтобы рекурсивные вызовы выглядели как рекурсивные вызовы.

LaTeX

$$$\\mathrm{corec}_1\\ g\\ x = \\mathrm{Cofix.corec'} (\\lambda X. g \\; (\\mathrm{Sum.inl} \\; X) \\; (\\mathrm{Sum.inr} \\; x))$$$

Lean4

/-- Corecursor for `Cofix F`. The shape allows recursive calls to
look like recursive calls. -/
def corec₁ {α : TypeVec n} {β : Type u} (g : ∀ {X}, (Cofix F α → X) → (β → X) → β → F (α ::: X)) (x : β) : Cofix F α :=
  Cofix.corec' (fun x => g Sum.inl Sum.inr x) x

Похожие утверждения