🥁🩸😓 time

Now it is just a small matter of updating the docs, other minor occurrences of cmp and making the PR.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord. 5 files changed, 319 insertions(+), 298 deletions(-) It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord. 5 files changed, 319 insertions(+), 298 deletions(-) It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Done rewriting RBSet, RBMap, their theorems and operations to use Ord.

5 files changed, 319 insertions(+), 298 deletions(\-)

It is now usable as it is. I now have to get rid of cmp in WF (Well-formedness) too.

Defeated the termination checker of Lean 4 for the first time in my life.

I love summer

Goodness gracious. Wouldn't you look at that. It seems like Batteries.RBSet is missing a Decidable membership instance. An opportunity for me to contribute and apply my newly gained knowledge.

By the way, I don't regret the time spent doing this at all. I think this was an INVALUABLE EXPERIENCE and a good challenge overall. Really the thing I miss in my daily job.