mk — Mathlib · SciLib

English

Constructor for Cofix F. Given a shape in F (α :: Append1 Cofix F α), construct a Cofix F α.

Русский

Конструктор Cofix F. По данным форме в F (α ::: Cofix F α) строит Cofix F α.

LaTeX

$$$\\mathrm{mk} : F (\\alpha\\append1 \\mathrm{Cofix}\\,F\\,\\alpha) \to \\mathrm{Cofix}\\,F\\,\\alpha$$$

Lean4

/-- constructor for `Cofix F` -/
def mk {α : TypeVec n} : F (α.append1 <| Cofix F α) → Cofix F α :=
  Cofix.corec fun x => (appendFun id fun i : Cofix F α => Cofix.dest.{u} i) <$$> x

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