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

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

Equations

• Lean.SSet α = Lean.SMap α Unit

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

Equations

• Lean.SSet.instInhabited = inferInstanceAs (Inhabited (Lean.SMap α Unit))

@[reducible, inline]

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

Equations

• Lean.SSet.empty = Lean.SMap.empty

@[reducible, inline]

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

Equations

• s.insert a = Lean.SMap.insert s a ()

@[reducible, inline]

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

Equations

• s.contains a = Lean.SMap.contains s a

@[reducible, inline]

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

Equations

• s.forM f = Lean.SMap.forM s fun (a : α) (x : Unit) => f a

@[reducible, inline]

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

Move from stage 1 into stage 2.

Equations

• s.switch = Lean.SMap.switch s

@[reducible, inline]

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

Equations

• Lean.SSet.fold f init s = Lean.SMap.fold (fun (d : σ) (a : α) (x : Unit) => f d a) init s

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

Equations

• m.toList = Lean.SSet.fold (fun (es : List α) (a : α) => a :: es) [] m

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

Equations

• es.toSSet = List.foldl (fun (s : Lean.SSet α) (a : α) => s.insert a) { } es

instance instReprSSet {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} [Repr α] : Repr (Lean.SSet α)

Equations

• instReprSSet = { reprPrec := fun (v : Lean.SSet α) (prec : Nat) => Repr.addAppParen (reprArg v.toList ++ Std.Format.text ".toSSet") prec }