corecF — Mathlib

English

corecF constructs a corecursive value by feeding back the representation of g: β → F(α ⊕ β) into the M-type constructor.

Русский

corecF строит коррекурсивное значение, используя представление g: β → F(α ⊕ β) в конструкторе M-типа.

LaTeX

$$$$ \\mathrm{corecF}\\; g\\; x = \\mathrm{M}.\\mathrm{corec} \\_\\; (\\lambda t. \\mathrm{repr}(g\\, t))\\; x. $$$$

Lean4

/-- `corecF` is used as a basis for defining the corecursor of `Cofix F α`. `corecF`
uses corecursion to construct the M-type generated by `q.P` and uses function on `F`
as a corecursive step -/
def corecF {α : TypeVec n} {β : Type u} (g : β → F (α.append1 β)) : β → q.P.M α :=
  M.corec _ fun x => repr (g x)

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