diff --git a/src/Lean/Data/SSet.lean b/src/Lean/Data/SSet.lean
new file mode 100644
index 0000000000..de5ff9540f
--- /dev/null
+++ b/src/Lean/Data/SSet.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Data.SMap
+
+namespace Lean
+
+/- Staged set. It is just a simple wrapper on top of Staged maps. -/
+
+def SSet (α : Type u) [BEq α] [Hashable α] := SMap α Unit
+
+namespace SSet
+variable {α : Type u} [BEq α] [Hashable α]
+
+instance : Inhabited (SSet α) := inferInstanceAs (Inhabited (SMap ..))
+
+abbrev empty : SSet α := SMap.empty
+
+abbrev insert (s : SSet α) (a : α) : SSet α :=
+  SMap.insert s a ()
+
+abbrev contains (s : SSet α) (a : α) : Bool :=
+  SMap.contains s a
+
+abbrev forM [Monad m] (s : SSet α) (f : α → m PUnit) : m PUnit :=
+  SMap.forM s fun a _ => f a
+
+/- Move from stage 1 into stage 2. -/
+abbrev switch (s : SSet α) : SSet α :=
+  SMap.switch s
+
+abbrev fold (f : σ → α → σ) (init : σ) (s : SSet α) : σ :=
+  SMap.fold (fun d a _ => f d a) init s
+
+abbrev size (s : SSet α) : Nat :=
+  SMap.size s
+
+def toList (m : SSet α) : List α :=
+  m.fold (init := []) fun es a => a::es
+
+end SSet
+
+end Lean
+
+def List.toSSet [BEq α] [Hashable α] (es : List α) : Lean.SSet α :=
+  es.foldl (init := {}) fun s a => s.insert a
+
+instance {_ : BEq α} {_ : Hashable α} [Repr α] : Repr (Lean.SSet α) where
+  reprPrec v prec := Repr.addAppParen (reprArg v.toList ++ ".toSSet") prec