list_getElem?₁ — Mathlib

English

For any list l, the function l[·]? : ℕ → Option α is primitive recursive.

Русский

Для любого списка l функция l[·]? : ℕ → Option α примрrec.

LaTeX

$$$$ \\forall l.\\ \\mathrm{Primrec}(l[\\cdot]? : \\mathbb{N} \\to \\mathrm{Option}(\\alpha)) $$$$

Lean4

theorem list_getElem?₁ : ∀ l : List α, Primrec (l[·]? : ℕ → Option α)
  | [] => dom_denumerable.2 zero
  | a :: l =>
    dom_denumerable.2 <|
      (casesOn1 (encode a).succ <| dom_denumerable.1 <| list_getElem?₁ l).of_eq fun n => by cases n <;> simp

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