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]