[Merged by Bors] - chore(data/hash_map): linting

[kmill]

No description provided.

[robertylewis]

Could you add an "implementation details" section that says a little bit about the construction? In particular, they're built around arrays, which have some overhead. The VM will destructively update arrays when there's only a single reference, but Lean's reference counting is pretty opaque and hard to predict.

[kmill]

I added some more detail based on my understanding of the implementation.

[digama0]

@robertylewis When this structure was written, arrays were implemented in C++ as parray, which has fairly good performance even if the array is shared, by strategically deferring updates in some way. I recall there being a push to replace that with plain arrays, which have a much worse performance cliff if you aren't careful to use the value linearly, but I forget if that ever landed.

[robertylewis]

@digama0 It's probably been at least two years since I tried to use hash_map or array but I remember having major issues last time. Is the doc string here accurate to your understanding?

[gebner]

@digama0 No, that change never landed. Particularly with monads it was very easy to cause non-linearity.

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests