chore: Inhabited instances for Std.HashMap

src/Std/Data/DHashMap/Basic.lean

@@ -63,6 +63,9 @@ namespace DHashMap
 instance [BEq α] [Hashable α] : EmptyCollection (DHashMap α β) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (DHashMap α β) where
+  default := ∅
+
 @[inline, inherit_doc Raw.insert] def insert [BEq α] [Hashable α] (m : DHashMap α β) (a : α)
     (b : β a) : DHashMap α β :=
   ⟨Raw₀.insert ⟨m.1, m.2.size_buckets_pos⟩ a b, .insert₀ m.2⟩

src/Std/Data/DHashMap/Raw.lean

@@ -54,6 +54,9 @@ capacity.
 instance : EmptyCollection (Raw α β) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α β) where
+  default := ∅
+
 /--
 Inserts the given mapping into the map, replacing an existing mapping for the key if there is one.
 -/

src/Std/Data/HashMap/Basic.lean

@@ -66,6 +66,9 @@ namespace HashMap
 instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (HashMap α β) where
+  default := ∅
+
 @[inline, inherit_doc DHashMap.insert] def insert [BEq α] [Hashable α] (m : HashMap α β) (a : α)
     (b : β) : HashMap α β :=
   ⟨m.inner.insert a b⟩

src/Std/Data/HashMap/Raw.lean

@@ -63,6 +63,9 @@ namespace Raw
 instance : EmptyCollection (Raw α β) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α β) where
+  default := ∅
+
 @[inline, inherit_doc DHashMap.Raw.insert] def insert [BEq α] [Hashable α] (m : Raw α β) (a : α)
     (b : β) : Raw α β :=
   ⟨m.inner.insert a b⟩

src/Std/Data/HashSet/Basic.lean

@@ -64,6 +64,9 @@ capacity.
 instance [BEq α] [Hashable α] : EmptyCollection (HashSet α) where
   emptyCollection := empty
 
+instance [BEq α] [Hashable α] : Inhabited (HashSet α) where
+  default := ∅
+
 /--
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

src/Std/Data/HashSet/Raw.lean

@@ -65,6 +65,9 @@ the empty collection notations `∅` and `{}` to create an empty hash set with t
 instance : EmptyCollection (Raw α) where
   emptyCollection := empty
 
+instance : Inhabited (Raw α) where
+  default := ∅
+
 /--
 Inserts the given element into the set. If the hash set already contains an element that is
 equal (with regard to `==`) to the given element, then the hash set is returned unchanged.