English
O(log n). Split a tree at the i-th element, producing a pair (left, right) such that left contains the first i elements and right contains the rest.
Русский
O(log n). Разбить дерево на позицию i, получив пару (левая, правая), где левая содержит первые i элементов, а правая — остальные.
LaTeX
$$$$ \mathrm{splitAt}: \mathbb{N} \to \ Ordnode\; \alpha \to \ Ordnode\; \alpha \times \ Ordnode\; \alpha, \quad \mathrm{splitAt}(i,t) = \begin{cases} (t, \text{nil}) & |t| \le i \\ \mathrm{splitAtAux}(t,i) & \text{иначе} \end{cases} $$$$
Lean4
/-- O(log n). Split a set at the `i`th element, getting the first `i` and everything else.
splitAt 2 {a, b, c, d} = ({a, b}, {c, d})
splitAt 5 {a, b, c, d} = ({a, b, c, d}, ∅) -/
def splitAt (i : ℕ) (t : Ordnode α) : Ordnode α × Ordnode α :=
if size t ≤ i then (t, nil) else splitAtAux t i
