doc: mention linearity in hash map docstring (#4771)

src/Std/Data/DHashMap/Basic.lean

@@ -44,6 +44,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the

src/Std/Data/DHashMap/RawDef.lean

@@ -26,16 +26,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `DHashMap.Raw`. Lemmas about the operations on `Std.Data.DHashMap.Raw` are available in the
 module `Std.Data.DHashMap.RawLemmas`.
 
-The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
-the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
-should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
-`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
-instance is lawful, i.e., if `a == b` implies `a = b`.
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
 
 This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
 and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
+
+The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
+the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
+should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
+`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
+instance is lawful, i.e., if `a == b` implies `a = b`.
 -/
 structure Raw (α : Type u) (β : α → Type v) where
   /-- The number of mappings present in the hash map -/

src/Std/Data/HashMap/Basic.lean

@@ -39,6 +39,9 @@ and an array of buckets, where each bucket is a linked list of key-value pais. T
 is always a power of two. The hash map doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the

src/Std/Data/HashMap/Raw.lean

@@ -37,17 +37,20 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `HashMap.Raw`. Lemmas about the operations on `Std.Data.HashMap.Raw` are available in the
 module `Std.Data.HashMap.RawLemmas`.
 
+This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
+and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
+is always a power of two. The hash map doubles its size upon inserting an element such that the
+number of elements is more than 75% of the number of buckets.
+
+The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
+avoid expensive copies.
+
 The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
 `EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
 instance is lawful, i.e., if `a == b` implies `a = b`.
 
-This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
-and an array of buckets, where each bucket is a linked list of key-value pais. The number of buckets
-is always a power of two. The hash map doubles its size upon inserting an element such that the
-number of elements is more than 75% of the number of buckets.
-
 Dependent hash maps, in which keys may occur in their values' types, are available as
 `Std.Data.Raw.DHashMap`.
 -/

src/Std/Data/HashSet/Basic.lean

@@ -35,6 +35,9 @@ and an array of buckets, where each bucket is a linked list of keys. The number
 is always a power of two. The hash set doubles its size upon inserting an element such that the
 number of elements is more than 75% of the number of buckets.
 
+The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
+avoid expensive copies.
+
 The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the

src/Std/Data/HashSet/Raw.lean

@@ -37,16 +37,19 @@ inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt
 over `HashSet.Raw`. Lemmas about the operations on `Std.Data.HashSet.Raw` are available in the
 module `Std.Data.HashSet.RawLemmas`.
 
+This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
+and an array of buckets, where each bucket is a linked list of keys. The number of buckets
+is always a power of two. The hash set doubles its size upon inserting an element such that the
+number of elements is more than 75% of the number of buckets.
+
+The hash table is backed by an `Array`. Users should make sure that the hash set is used linearly to
+avoid expensive copies.
+
 The hash set uses `==` (provided by the `BEq` typeclass) to compare elements and `hash` (provided by
 the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
 should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
 `EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
 instance is lawful, i.e., if `a == b` implies `a = b`.
-
-This is a simple separate-chaining hash table. The data of the hash set consists of a cached size
-and an array of buckets, where each bucket is a linked list of keys. The number of buckets
-is always a power of two. The hash set doubles its size upon inserting an element such that the
-number of elements is more than 75% of the number of buckets.
 -/
 structure Raw (α : Type u) where
   /-- Internal implementation detail of the hash set. -/