list_idxOf₁ — Mathlib

English

If α has decidable equality, the function a ↦ List.idxOf a l is primitive recursive.

Русский

Если для типа α существуетDecidableEq, функция a ↦ List.idxOf a l примитивно рекурсивна.

LaTeX

$$$[DecidableEq\\alpha] (l:\\mathrm{List}\\alpha) \\Rightarrow \\Primrec (\\lambda a. \\mathrm{List.idxOf}\\ a\\ l)$$$

Lean4

theorem list_idxOf₁ [DecidableEq α] (l : List α) : Primrec fun a => l.idxOf a :=
  list_findIdx₁ (.swap .beq) l

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