list_foldr — Mathlib

English

List.foldr is primitive recursive if the corresponding operations are primitive recursive.

Русский

Свёртка справа по списку примитивно вычислима, если соответствующие операции примитивно вычислимы.

LaTeX

$$$\\mathrm{Primrec}\\left( f,g,h \\mapsto \\text{(foldr along f with }g\\text{ and }h) }\\right)$$$

Lean4

theorem list_foldr {f : α → List β} {g : α → σ} {h : α → β × σ → σ} (hf : Primrec f) (hg : Primrec g)
    (hh : Primrec₂ h) : Primrec fun a => (f a).foldr (fun b s => h a (b, s)) (g a) :=
  (list_foldl (list_reverse.comp hf) hg <| to₂ <| hh.comp fst <| (pair snd fst).comp snd).of_eq fun a => by
    simp [List.foldl_reverse]

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