Zulip Chat Archive

Stream: general

Topic: rbmap


Chris Hughes (Dec 13 2020 at 15:18):

Is this something in core that basically shouldn't be used? I noticed there's no rbmap.erase which would be very handy.

Chris Hughes (Dec 13 2020 at 15:23):

If it shouldn't be used, what's the best thing to use instead?

Mario Carneiro (Dec 13 2020 at 15:25):

I started working on ordmap for this reason

Chris Hughes (Dec 13 2020 at 15:52):

What's the best alternative?

Mario Carneiro (Dec 13 2020 at 16:00):

do you need proofs? If no, you can use native.rb_map

Mario Carneiro (Dec 13 2020 at 16:01):

If yes, you might find it easiest to work with alist

Mario Carneiro (Dec 13 2020 at 16:02):

I'm currently working on updating the ordmap branch, which was left unmerged 2 years ago and so needs a bit of bitrot treatment

Mario Carneiro (Dec 13 2020 at 16:02):

the proofs are not complete but the data structure itself works fine

Chris Hughes (Dec 13 2020 at 16:20):

I don't need proofs, I'll use native.rbmap thanks

Chris Hughes (Dec 13 2020 at 16:31):

It's a bit annoying that rb_map.min only returns data and not a key. Is this standard?

Mario Carneiro (Dec 13 2020 at 16:38):

I'm afraid that native.rb_map is kind of take it or leave it, unless you want to add more ops in the C++


Last updated: Dec 20 2023 at 11:08 UTC