corec — Mathlib

English

Define the corecursor for the M-type by combining the components with a tail recursion using M.corec' and the projections drop and last.

Русский

Определение корекурсора для M‑типа через сочетание компонент с хвостовой рекурсией, используя M.corec'.

LaTeX

$$$\\text{corec} : (P : MvPFunctor (n+1)) \\to {α} {β} \\to (g : β → P (α.append1 β)) → β → P.M α$$$

Lean4

/-- Corecursor for M-type of `P` -/
def corec {α : TypeVec n} {β : Type u} (g : β → P (α.append1 β)) : β → P.M α :=
  M.corec' P (fun b => (g b).fst) (fun b => dropFun (g b).snd) fun b => lastFun (g b).snd

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