list_casesOn — Mathlib

English

List.casesOn is primitive recursive: it performs a case split on a list according to head and tail.

Русский

List.casesOn является примитивно вычислимым: выполняет разбор списка по головному элементу и остальной части.

LaTeX

$$$\\mathrm{Primrec}\\left( a \\mapsto \\mathrm{List.casesOn}\\left( f(a) \\right) \\left( g(a) \\right) \\left( \\lambda b\\ l. h(a)(b,l) \\right) \\right)$$$

Lean4

theorem list_casesOn {f : α → List β} {g : α → σ} {h : α → β × List β → σ} :
    Primrec f → Primrec g → Primrec₂ h → @Primrec _ σ _ _ fun a => List.casesOn (f a) (g a) fun b l => h a (b, l) :=
  list_casesOn' (Primcodable.prim _)

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