From bf1ea58deb2749601ef47d8022f1697641bbe678 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 27 Oct 2019 11:35:23 -0700
Subject: [PATCH] feat: add `HashSet`

It is just a wrapper for `HashMap`
---
 library/Init/Data/HashMap/Basic.lean |  5 ++-
 library/Init/Data/HashSet.lean       | 51 ++++++++++++++++++++++++++++
 2 files changed, 55 insertions(+), 1 deletion(-)
 create mode 100644 library/Init/Data/HashSet.lean

diff --git a/library/Init/Data/HashMap/Basic.lean b/library/Init/Data/HashMap/Basic.lean
index 859fa3fc86..fd80061656 100644
--- a/library/Init/Data/HashMap/Basic.lean
+++ b/library/Init/Data/HashMap/Basic.lean
@@ -170,9 +170,12 @@ match m with
 match m with
 | ⟨ {size := sz, ..}, _ ⟩ => sz
 
-@[inline] def empty (m : HashMap α β) : Bool :=
+@[inline] def isEmpty (m : HashMap α β) : Bool :=
 m.size = 0
 
+@[inline] def empty : HashMap α β :=
+mkHashMap
+
 def numBuckets (m : HashMap α β) : Nat :=
 m.val.buckets.val.size
 
diff --git a/library/Init/Data/HashSet.lean b/library/Init/Data/HashSet.lean
new file mode 100644
index 0000000000..60bd0d8db7
--- /dev/null
+++ b/library/Init/Data/HashSet.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Leonardo de Moura
+-/
+prelude
+import Init.Data.HashMap
+
+universes u v
+
+structure HashSet (α : Type u) [HasBeq α] [Hashable α] :=
+(set : HashMap α Unit)
+
+def mkHashSet {α : Type u} [HasBeq α] [Hashable α] (nbuckets := 8) : HashSet α :=
+{ set := mkHashMap nbuckets }
+
+namespace HashSet
+
+variables {α : Type u} [HasBeq α] [Hashable α]
+
+instance : Inhabited (HashSet α) :=
+⟨mkHashSet⟩
+
+instance : HasEmptyc (HashSet α) :=
+⟨mkHashSet⟩
+
+@[inline] def insert (s : HashSet α) (a : α) : HashSet α :=
+{ set := s.set.insert a () }
+
+@[inline] def erase (s : HashSet α) (a : α) : HashSet α :=
+{ set := s.set.erase a }
+
+@[inline] def contains (s : HashSet α) (a : α) : Bool :=
+s.set.contains a
+
+@[inline] def size (s : HashSet α) : Nat :=
+s.set.size
+
+@[inline] def isEmpty (s : HashSet α) : Bool :=
+s.set.isEmpty
+
+@[inline] def empty : HashSet α :=
+mkHashSet
+
+@[inline] def mfold {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (d : β) (s : HashSet α) : m β :=
+s.set.mfold (fun d a _ => f d a) d
+
+@[inline] def fold {β : Type v} (f : β → α → β) (d : β) (s : HashSet α) : β :=
+Id.run $ s.mfold f d
+
+end HashSet