recF — Mathlib

English

recF is a recursion operator for Fix F α: it traverses the W-type generated by q.P using a recursive step given by g.

Русский

recF — это рекурсивный оператор для Fix F α: он обходит W-тип, порождаемый q.P, используя рекурсивный шаг, данный функцией g.

LaTeX

$$$\mathrm{recF}(g) := q.P.W\;\alpha \to \beta \quad\text{defined by }\; q.P.wRec(\surd).$$$

Lean4

/-- `recF` is used as a basis for defining the recursor on `Fix F α`. `recF`
traverses recursively the W-type generated by `q.P` using a function on `F`
as a recursive step -/
def recF {α : TypeVec n} {β : Type u} (g : F (α.append1 β) → β) : q.P.W α → β :=
  q.P.wRec fun a f' _f rec => g (abs ⟨a, splitFun f' rec⟩)

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