Dean Young (Sep 13 2022 at 14:48):
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 (Sep 13 2022 at 15:11):
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 (Sep 13 2022 at 15:16):
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 (Sep 13 2022 at 15:18):
Dean Young (Sep 13 2022 at 15:19):
oh wow those worked! Thanks Jannis you're the best.
Mario Carneiro (Sep 13 2022 at 17:58):
Lean 3 also has a hashmap implementation, very similar to std.hashmap: docs#hash_map
Last updated: Aug 03 2023 at 10:10 UTC