English
There is a function splitMax that, if the tree is nonempty, returns the tree with the maximum element removed together with that maximum element; otherwise returns none.
Русский
Существует функция splitMax, которая, если дерево непустое, возвращает дерево без максимального элемента и сам максимум; иначе — none.
LaTeX
$$$$ \mathrm{splitMax}: \ Ordnode\; \alpha \to \mathrm{Option}(\mathrm Ordnode\; \alpha \times \alpha), \\ \mathrm{splitMax}(nil) = \mathrm{none}, \\ \mathrm{splitMax}(\mathrm{node}\; sz\; l\; x\; r) = \mathrm{splitMax'}(x, l, r) $$$$
Lean4
/-- O(log n). Extract and remove the maximum element from the tree, if it exists.
split_max {1, 2, 3} = some ({1, 2}, 3)
split_max ∅ = none -/
def splitMax : Ordnode α → Option (Ordnode α × α)
| nil => none
| node _ x l r => splitMax' x l r
