English
Auxiliary function for take. It returns the subtree containing the first i elements of t, or empty if i=0.
Русский
Вспомогательная функция take. Возвращает поддерево, содержащее первые i элементов дерева, или пустое, если i=0.
LaTeX
$$$$ \mathrm{takeAux}: \ Ordnode\; \alpha \to \mathbb{N} \to \ Ordnode\; \alpha, \\ \mathrm{takeAux}(\mathrm nil, i) = \mathrm nil, \\ \mathrm{takeAux}(\mathrm node\; l\; x\; r, i) = \begin{cases} \mathrm nil & i=0 \\ \mathrm{link}\; l\; x\; (\mathrm{takeAux}\; r\; j) & \text{where } j = i - |l| - 1 \text{ if } i>|l|+1 \end{cases} $$$$
Lean4
/-- Auxiliary definition for `take`. (Can also be used in lieu of `take` if you know the
index is within the range of the data structure.)
takeAux {a, b, c, d} 2 = {a, b}
takeAux {a, b, c, d} 5 = {a, b, c, d} -/
def takeAux : Ordnode α → ℕ → Ordnode α
| nil, _ => nil
| node _ l x r, i =>
if i = 0 then nil
else
match Nat.psub' i (size l) with
| none => takeAux l i
| some 0 => l
| some (j + 1) => link l x (takeAux r j)
