def Lean.SSet (α : Type u) [BEq α] [Hashable α] : Type u

Staged set. It is just a simple wrapper on top of Staged maps.

instance Lean.SSet.instInhabitedSSet {α : Type u} [BEq α] [Hashable α] : Inhabited (Lean.SSet α)

@[inline, reducible]

abbrev Lean.SSet.empty {α : Type u} [BEq α] [Hashable α] : Lean.SSet α

@[inline, reducible]

abbrev Lean.SSet.insert {α : Type u} [BEq α] [Hashable α] (s : Lean.SSet α) (a : α) : Lean.SSet α

@[inline, reducible]

abbrev Lean.SSet.contains {α : Type u} [BEq α] [Hashable α] (s : Lean.SSet α) (a : α) : Bool

@[inline, reducible]

abbrev Lean.SSet.forM {α : Type u} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} [Monad m] (s : Lean.SSet α) (f : α → m PUnit) : m PUnit

@[inline, reducible]

abbrev Lean.SSet.switch {α : Type u} [BEq α] [Hashable α] (s : Lean.SSet α) : Lean.SSet α

Move from stage 1 into stage 2.

@[inline, reducible]

abbrev Lean.SSet.fold {α : Type u} [BEq α] [Hashable α] {σ : Type u_1} (f : σ → α → σ) (init : σ) (s : Lean.SSet α) : σ

@[inline, reducible]

abbrev Lean.SSet.size {α : Type u} [BEq α] [Hashable α] (s : Lean.SSet α) : Nat

def Lean.SSet.toList {α : Type u} [BEq α] [Hashable α] (m : Lean.SSet α) : List α

def List.toSSet {α : Type u_1} [BEq α] [Hashable α] (es : List α) : Lean.SSet α

instance instReprSSet {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → [inst : Repr α] → Repr (Lean.SSet α)