From 4a24852f166330a48ed7d444e1dcdef279a3cd2d Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Mon, 13 Jan 2025 09:18:28 +0100
Subject: [PATCH] Move ofList out of unverified

---
 src/Std/Data/DHashMap/Basic.lean | 24 +++++++++++-----------
 src/Std/Data/DHashMap/Raw.lean   | 34 +++++++++++++++++---------------
 src/Std/Data/HashMap/Basic.lean  | 16 +++++++--------
 src/Std/Data/HashMap/Raw.lean    | 16 +++++++--------
 src/Std/Data/HashSet/Basic.lean  | 16 +++++++--------
 src/Std/Data/HashSet/Raw.lean    | 16 +++++++--------
 6 files changed, 62 insertions(+), 60 deletions(-)

diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 8ddbfd80216a..1f8ee095f152 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -297,24 +297,12 @@ but will later become a primitive operation.
   ⟨(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insertIfNew₀ m.2⟩
 
-@[inline, inherit_doc Raw.ofList] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
-    DHashMap α β :=
-  insertMany ∅ l
-
 /-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β :=
   m₂.fold (init := m₁) fun acc x => acc.insert x
 
 instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩
 
-@[inline, inherit_doc Raw.Const.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
-    (l : List (α × β)) : DHashMap α (fun _ => β) :=
-  Const.insertMany ∅ l
-
-@[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
-    DHashMap α (fun _ => Unit) :=
-  Const.insertManyIfNewUnit ∅ l
-
 @[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
     DHashMap α (fun _ => Unit) :=
   Const.insertManyIfNewUnit ∅ l
@@ -328,4 +316,16 @@ instance [BEq α] [Hashable α] [Repr α] [(a : α) → Repr (β a)] : Repr (DHa
 
 end Unverified
 
+@[inline, inherit_doc Raw.ofList] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
+    DHashMap α β :=
+  insertMany ∅ l
+
+@[inline, inherit_doc Raw.Const.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
+    (l : List (α × β)) : DHashMap α (fun _ => β) :=
+  Const.insertMany ∅ l
+
+@[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
+    DHashMap α (fun _ => Unit) :=
+  Const.insertManyIfNewUnit ∅ l
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index 8a6c7788c7b6..5319672f6692 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -422,10 +422,6 @@ This is mainly useful to implement `HashSet.insertMany`, so if you are consideri
     (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).1
   else m -- will never happen for well-formed inputs
 
-/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
-occurrence takes precedence. -/
-@[inline] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) : Raw α β :=
-  insertMany ∅ l
 
 /-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β :=
@@ -433,18 +429,6 @@ occurrence takes precedence. -/
 
 instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩
 
-@[inline, inherit_doc Raw.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
-    (l : List (α × β)) : Raw α (fun _ => β) :=
-  Const.insertMany ∅ l
-
-/-- Creates a hash map from a list of keys, associating the value `()` with each key.
-
-This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
-`HashSet` or `HashSet.Raw` might be a better fit for you. -/
-@[inline] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
-    Raw α (fun _ => Unit) :=
-  Const.insertManyIfNewUnit ∅ 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,
@@ -470,6 +454,24 @@ end Unverified
 @[inline] def keys (m : Raw α β) : List α :=
   m.foldRev (fun acc k _ => k :: acc) []
 
+/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
+occurrence takes precedence. -/
+@[inline] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) : Raw α β :=
+  insertMany ∅ l
+
+
+@[inline, inherit_doc Raw.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
+    (l : List (α × β)) : Raw α (fun _ => β) :=
+  Const.insertMany ∅ l
+
+/-- Creates a hash map from a list of keys, associating the value `()` with each key.
+
+This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
+`HashSet` or `HashSet.Raw` might be a better fit for you. -/
+@[inline] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
+    Raw α (fun _ => Unit) :=
+  Const.insertManyIfNewUnit ∅ l
+
 section WF
 
 /--
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 0063ae3e4839..a9060733e4ad 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -191,6 +191,14 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
 @[inline, inherit_doc DHashMap.keys] def keys (m : HashMap α β) : List α :=
   m.inner.keys
 
+@[inline, inherit_doc DHashMap.Const.ofList] def ofList [BEq α] [Hashable α] (l : List (α × β)) :
+    HashMap α β :=
+  ⟨DHashMap.Const.ofList l⟩
+
+@[inline, inherit_doc DHashMap.Const.unitOfList] def unitOfList [BEq α] [Hashable α] (l : List α) :
+    HashMap α Unit :=
+  ⟨DHashMap.Const.unitOfList l⟩
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -269,20 +277,12 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
     {ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
   ⟨DHashMap.Const.insertManyIfNewUnit m.inner l⟩
 
-@[inline, inherit_doc DHashMap.Const.ofList] def ofList [BEq α] [Hashable α] (l : List (α × β)) :
-    HashMap α β :=
-  ⟨DHashMap.Const.ofList l⟩
-
 /-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β :=
   m₂.fold (init := m₁) fun acc x => acc.insert x
 
 instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩
 
-@[inline, inherit_doc DHashMap.Const.unitOfList] def unitOfList [BEq α] [Hashable α] (l : List α) :
-    HashMap α Unit :=
-  ⟨DHashMap.Const.unitOfList l⟩
-
 @[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) :
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfArray l⟩
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 91718cb8f368..5db2a768e678 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -173,6 +173,14 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
 @[inline, inherit_doc DHashMap.Raw.keys] def keys (m : Raw α β) : List α :=
   m.inner.keys
 
+@[inline, inherit_doc DHashMap.Raw.Const.ofList] def ofList [BEq α] [Hashable α]
+    (l : List (α × β)) : Raw α β :=
+  ⟨DHashMap.Raw.Const.ofList l⟩
+
+@[inline, inherit_doc DHashMap.Raw.Const.unitOfList] def unitOfList [BEq α] [Hashable α]
+    (l : List α) : Raw α Unit :=
+  ⟨DHashMap.Raw.Const.unitOfList l⟩
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -233,20 +241,12 @@ m.inner.values
     [Hashable α] {ρ : Type w} [ForIn Id ρ α] (m : Raw α Unit) (l : ρ) : Raw α Unit :=
   ⟨DHashMap.Raw.Const.insertManyIfNewUnit m.inner l⟩
 
-@[inline, inherit_doc DHashMap.Raw.Const.ofList] def ofList [BEq α] [Hashable α]
-    (l : List (α × β)) : Raw α β :=
-  ⟨DHashMap.Raw.Const.ofList l⟩
-
 /-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β :=
   m₂.fold (init := m₁) fun acc x => acc.insert x
 
 instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩
 
-@[inline, inherit_doc DHashMap.Raw.Const.unitOfList] def unitOfList [BEq α] [Hashable α]
-    (l : List α) : Raw α Unit :=
-  ⟨DHashMap.Raw.Const.unitOfList l⟩
-
 @[inline, inherit_doc DHashMap.Raw.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α]
     (l : Array α) : Raw α Unit :=
   ⟨DHashMap.Raw.Const.unitOfArray l⟩
diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean
index bbbb3517b4dd..2a75fd63fc39 100644
--- a/src/Std/Data/HashSet/Basic.lean
+++ b/src/Std/Data/HashSet/Basic.lean
@@ -162,6 +162,14 @@ for all `a`.
 @[inline] def toList (m : HashSet α) : List α :=
   m.inner.keys
 
+/--
+Creates a hash set from a list 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 ofList [BEq α] [Hashable α] (l : List α) : HashSet α :=
+  ⟨HashMap.unitOfList l⟩
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -233,14 +241,6 @@ appearance.
     HashSet α :=
   ⟨m.inner.insertManyIfNewUnit l⟩
 
-/--
-Creates a hash set from a list 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 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
diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean
index d0a7dd010fcf..699dd5c8e66d 100644
--- a/src/Std/Data/HashSet/Raw.lean
+++ b/src/Std/Data/HashSet/Raw.lean
@@ -165,6 +165,14 @@ for all `a`.
 @[inline] def toList (m : Raw α) : List α :=
   m.inner.keys
 
+/--
+Creates a hash set from a list 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 ofList [BEq α] [Hashable α] (l : List α) : Raw α :=
+  ⟨HashMap.Raw.unitOfList l⟩
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -231,14 +239,6 @@ appearance.
     Raw α :=
   ⟨m.inner.insertManyIfNewUnit l⟩
 
-/--
-Creates a hash set from a list 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 ofList [BEq α] [Hashable α] (l : List α) : Raw α :=
-  ⟨HashMap.Raw.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