From f0c59364f49f94bac8a8fd7d6d998d84b817128a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 2 Jan 2025 04:52:21 +0100
Subject: [PATCH] feat: add `PersistentHashSet.toList` (#6501)

This PR adds `PersistentHashSet.toList`
---
 src/Lean/Data/PersistentHashSet.lean | 5 +++++
 1 file changed, 5 insertions(+)

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