unbalanced RBMap and RBSet

Stream: lean4

[Arthur Paulino]

Does inserting elements with monotonically increasing/decreasing keys causes those structures to become unbalanced or do they have some self-balancing heuristic?

[Arthur Paulino]

Ah, I'm asking about the Std versions specifically

[Sebastian Ullrich]

The implementation is in the name :) . Red-black trees are self-balancing.

[Arthur Paulino]

Thanks, I didn't know that