English
O(log n). Drop the first i elements of the tree, returning the remaining subtree; if i exceeds the size, return empty.
Русский
O(log n). Удаляем первые i элементов дерева, возвращая оставшееся поддерево; если i больше размера, вернуть пустое дерево.
LaTeX
$$$$ \mathrm{drop}(i,t) = \begin{cases} \mathrm{nil} & \text{если } |t| \le i \\ \mathrm{dropAux}(t,i) & \text{иначе} \end{cases} $$$$
Lean4
/-- O(log n). Remove the first `i` elements of the set, counted from the left.
drop 2 {a, b, c, d} = {c, d}
drop 5 {a, b, c, d} = ∅ -/
def drop (i : ℕ) (t : Ordnode α) : Ordnode α :=
if size t ≤ i then nil else dropAux t i
