findIndex — Mathlib

English

O(log n). Get the index of an element equivalent to x in the tree, if it exists.

Русский

O(log n). Найти индекс элемента, эквивалентного x, в дереве, если он существует.

LaTeX

$$$$ \mathrm{findIndex}: (x: \alpha) \to \ Ordnode\; \alpha \to \mathrm{Option}\; \mathbb{N}, \quad \mathrm{findIndex}(x,t) = \mathrm{findIndexAux}(x,t,0) $$$$

Lean4

/-- O(log n). Get the index, counting from the left,
of an element equivalent to `x` if it exists.

    findIndex 2 {1, 2, 4} = some 1
    findIndex 4 {1, 2, 4} = some 2
    findIndex 5 {1, 2, 4} = none -/
def findIndex (x : α) (t : Ordnode α) : Option ℕ :=
  findIndexAux x t 0

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