diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 42daaa7743..f1a8a032be 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -269,6 +269,10 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh 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 diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 9d0d96b905..cf604f0910 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -411,6 +411,14 @@ This is mainly useful to implement `HashSet.ofList`, so if you are considering u 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 diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index f68cc9520b..e3a1c549cc 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -255,6 +255,10 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β 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 diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 4c2ee8fcf6..184f6fa88c 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -217,6 +217,14 @@ in the collection will be present in the returned hash set. @[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