Lean.Data.SSet

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

m PUnit

Equations

Lean.SSet.forM s f = Lean.SMap.forM s fun a x => f a

source

@[inline]

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

Lean.SSet α

Equations

Lean.SSet.switch s = Lean.SMap.switch s

source

@[inline]

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

σ

Equations

Lean.SSet.fold f init s = Lean.SMap.fold (fun d a x => f d a) init s

source

@[inline]

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

Nat

Equations

Lean.SSet.size s = Lean.SMap.size s

source

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

List α

Equations

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

source

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

Lean.SSet α

Equations

List.toSSet es = List.foldl (fun s a => Lean.SSet.insert s a) { stage₁ := true, map₁ := ∅, map₂ := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } es

source

instance instReprSSet {α : Type u_1} :

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

Equations

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