corec' — Mathlib

English

Provide a corecursor for the M-type: a function that, given a seed and steps, returns an element of M α.

Русский

Обеспечить корекурсор для M‑типа: функция, которая, имея зерно и шаги, возвращает элемент M α.

LaTeX

$$$\\text{corec'} : (P : MvPFunctor (n+1)) \\to {α} {β} \\to (g_0,g_1,g_2) \\to \\mathbb{N} \\to M α$$$

Lean4

/-- Corecursor for M-type of `P` -/
def corec' {α : TypeVec n} {β : Type u} (g₀ : β → P.A) (g₁ : ∀ b : β, P.drop.B (g₀ b) ⟹ α)
    (g₂ : ∀ b : β, P.last.B (g₀ b) → β) : β → P.M α := fun b =>
  ⟨M.corecShape P g₀ g₂ b, M.corecContents P g₀ g₁ g₂ _ _ rfl⟩

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