English
Auxiliary definition for findIndex. It returns the (optional) index of an element equivalent to x in the tree.
Русский
Вспомогательная функция для findIndex. Возвращает необязательный индекс элемента, эквивалентного x, в дереве.
LaTeX
$$$$ \mathrm{findIndexAux}: (x: \alpha) \to \ Ordnode\; \alpha \to \mathbb{N} \to \mathrm{Option}\; \mathbb{N}, \quad \mathrm{findIndexAux}(x, nil, i) = \text{none}, \\ \mathrm{findIndexAux}(x, \mathrm{node}\; l\; y\; r, i) = \begin{cases} \mathrm{findIndexAux}(x, l, i) & x < y \\ \mathrm{some}(i + \lvert l \rvert) & x = y \\ \mathrm{findIndexAux}(x, r, i + |l| + 1) & x > y \end{cases} $$$$
Lean4
/-- Auxiliary definition for `findIndex`. -/
def findIndexAux (x : α) : Ordnode α → ℕ → Option ℕ
| nil, _ => none
| node _ l y r, i =>
match cmpLE x y with
| Ordering.lt => findIndexAux x l i
| Ordering.eq => some (i + size l)
| Ordering.gt => findIndexAux x r (i + size l + 1)
