diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean
index ec57ff612b65..206e3fce365d 100644
--- 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