English
Auxiliary definition for splitAt. It partitions a tree into two trees at index i, returning (leftPart, rightPart).
Русский
Вспомогательное определение splitAt. Разбивает дерево на две части по индексу i, возвращая (левая, правая).
LaTeX
$$$$ \mathrm{splitAtAux}: \ Ordnode\; \alpha \to \mathbb{N} \to \ Ordnode\; \alpha \times \ Ordnode\; \alpha, \quad \text{случаи по дереву аналогично описанию} $$$$
Lean4
/-- Auxiliary definition for `splitAt`. (Can also be used in lieu of `splitAt` if you know the
index is within the range of the data structure.)
splitAtAux {a, b, c, d} 2 = ({a, b}, {c, d})
splitAtAux {a, b, c, d} 5 = ({a, b, c, d}, ∅) -/
def splitAtAux : Ordnode α → ℕ → Ordnode α × Ordnode α
| nil, _ => (nil, nil)
| t@(node _ l x r), i =>
if i = 0 then (nil, t)
else
match Nat.psub' i (size l) with
| none =>
let (l₁, l₂) := splitAtAux l i
(l₁, link l₂ x r)
| some 0 => (glue l r, insertMin x r)
| some (j + 1) =>
let (r₁, r₂) := splitAtAux r j
(link l x r₁, r₂)
