feat: add PersistentHashSet.toList (#6501)

This PR adds `PersistentHashSet.toList`
leanprover · Jan 2, 2025 · f0c5936 · f0c5936
1 parent c0d67e2
commit f0c5936
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean
@@ -49,3 +49,8 @@ variable {_ : BEq α} {_ : Hashable α}
 
 @[inline] def fold {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) : β :=
   Id.run $ s.foldM f init
+
+def toList (s : PersistentHashSet α) : List α :=
+  s.set.toList.map (·.1)
+
+end PersistentHashSet