Zulip Chat Archive

Stream: lean4

Topic: Swisstable for lean

Schrodinger ZHU Yifan (Sep 17 2023 at 15:44):

Long ago, I ported Rust's hashbrown to Lean as a POC. It recently got updated. (Since people are working on HTTP, I guess higher thrput HashMap/HashSet will matter in some cases).

I have several questions:

  1. Do we have an existing stateful hash interface similar to the one here?
  2. What are the conventional class instances for containers like HashMap? (I mean Inhabited/EmptyCollection/etc)?
  3. General suggestions (repo).

James Gallicchio (Sep 17 2023 at 18:33):

  1. The closest I know of is docs#RandomGen which is not quite the same
  2. There is no consistency among the interfaces for containers or maplike structures. This is a big missing component of Std.

Mario Carneiro (Sep 17 2023 at 18:39):

I'm not sure that's true. There is consistency, it's just that is to not use interfaces (except for Inhabited and EmptyCollection)

Last updated: Dec 20 2023 at 11:08 UTC