feat: HashSet.ofArray (unverified)

src/Std/Data/DHashMap/Basic.lean

diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 472c73f..8220983 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -260,6 +260,10 @@
     DHashMap α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+@[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    DHashMap α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 @[inherit_doc Raw.Internal.numBuckets] def Internal.numBuckets
     (m : DHashMap α β) : Nat :=
   Raw.Internal.numBuckets m.1

src/Std/Data/DHashMap/Raw.lean

diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index 9d0d96b..cf604f0 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -411,6 +411,14 @@
     Raw α (fun _ => Unit) :=
   Const.insertManyUnit ∅ l
 
+/-- Creates a hash map from an array of keys, associating the value `()` with each key.
+
+This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this,
+`HashSet` or `HashSet.Raw` might be a better fit for you. -/
+@[inline] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    Raw α (fun _ => Unit) :=
+  Const.insertManyUnit ∅ l
+
 /--
 Returns the number of buckets in the internal representation of the hash map. This function may be
 useful for things like monitoring system health, but it should be considered an internal

src/Std/Data/HashMap/Basic.lean

diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 973889e..558da0d 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -250,6 +250,10 @@
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
+@[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfArray l⟩
+
 @[inline, inherit_doc DHashMap.Internal.numBuckets] def Internal.numBuckets
     (m : HashMap α β) : Nat :=
   DHashMap.Internal.numBuckets m.inner

src/Std/Data/HashSet/Basic.lean

diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index a065598..e5f9dd3 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -212,6 +212,14 @@
 @[inline] def ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
   ⟨HashMap.unitOfList l⟩
 
+/--
+Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
+collection contains multiple elements that are equal (with regard to `==`), then the last element
+in the collection will be present in the returned hash set.
+-/
+@[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α :=
+  ⟨HashMap.unitOfArray l⟩
+
 /-- Computes the union of the given hash sets. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α :=
   m₂.fold (init := m₁) fun acc x => acc.insert x