hashmap

Stream: general

[Dean Young]

I'm looking for a hashmap type with (for all practical purposes) constant time lookup (and of course the ability to add f(a) = b, preferably in constant time as well). Unfortunately the literature on hashmaps doesn't give me complexity times.

Does anyone have a hashmap type they like to use?

[Jannis Limperg]

For Lean 3, I'm not aware of any efficient hashmap implementation. Lean 4 has two variants of hashmaps in the standard library: docs4#Std.HashMap and docs4#Std.PersistentHashMap. The first one is what one would usually call a hashmap and it has the usual amortised constant-time insert/lookup/delete.

[Dean Young]

thanks very much Jannis. I'm new here .... do you think you could direct me to the standard documentation for docs4 and lean4? Those links aren't working for me.

[Jannis Limperg]

Curious -- if you click on these links, they should take you to this URL and this URL. (This docs4 stuff is a Zulip feature which allows us to write abbreviations for certain classes of links.)

[Dean Young]

oh wow those worked! Thanks Jannis you're the best.

[Mario Carneiro]

Lean 3 also has a hashmap implementation, very similar to std.hashmap: docs#hash_map