Lean4
/-- O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by `f` must be equivalent to `x`.
alter f 0 {1, 2, 3} = {1, 2, 3} if f none = none
= {a, 1, 2, 3} if f none = some a
alter f 1 {1, 2, 3} = {2, 3} if f 1 = none
= {a, 2, 3} if f 1 = some a -/
def alter (f : Option α → Option α) (x : α) : Ordnode α → Ordnode α
| nil => Option.recOn (f none) nil Ordnode.singleton
| _t@(node sz l y r) =>
match cmpLE x y with
| Ordering.lt => balance (alter f x l) y r
| Ordering.eq =>
match f (some y) with
| none => glue l r
| some a => node sz l a r
| Ordering.gt => balance l y (alter f x r)
