Zulip Chat Archive

Stream: lean4

Topic: lookup table

Johan Commelin (Sep 22 2022 at 07:26):

I'm goofing around with a tiny little Lean 4 program. I need a lookup table. What are my options? I looked in Std.Data.* and only found BinomialHeap.

Alexander Bentkamp (Sep 22 2022 at 07:53):

How about Std.HashMap?

Mario Carneiro (Sep 22 2022 at 07:53):

It's Lean.HashMap for now

Mario Carneiro (Sep 22 2022 at 07:55):

I'm working on getting the lean data structures that used to be in Std back again, but in the meanwhile you can use the Lean versions

Mario Carneiro (Sep 22 2022 at 07:55):

There is also RBMap

Johan Commelin (Sep 22 2022 at 07:56):

Aah, thanks!

Last updated: Dec 20 2023 at 11:08 UTC