structure Lean.PersistentHashSet (α : Type u) [BEq α] [Hashable α] : Type u

• set : Lean.PersistentHashMap α Unit

@[inline, reducible]

abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] : Type u

Equations

• Lean.PHashSet α = Lean.PersistentHashSet α

@[inline]

def Lean.PersistentHashSet.empty {α : Type u_1} [BEq α] [Hashable α] : Lean.PersistentHashSet α

Equations

• Lean.PersistentHashSet.empty = { set := Lean.PersistentHashMap.empty }

instance Lean.PersistentHashSet.instInhabitedPersistentHashSet {α : Type u_1} [BEq α] [Hashable α] : Inhabited (Lean.PersistentHashSet α)

Equations

• Lean.PersistentHashSet.instInhabitedPersistentHashSet = { default := Lean.PersistentHashSet.empty }

instance Lean.PersistentHashSet.instEmptyCollectionPersistentHashSet {α : Type u_1} [BEq α] [Hashable α] : EmptyCollection (Lean.PersistentHashSet α)

Equations

• Lean.PersistentHashSet.instEmptyCollectionPersistentHashSet = { emptyCollection := Lean.PersistentHashSet.empty }

@[inline]

def Lean.PersistentHashSet.isEmpty {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → Bool

Equations

• Lean.PersistentHashSet.isEmpty s = Lean.PersistentHashMap.isEmpty s.set

@[inline]

def Lean.PersistentHashSet.insert {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α

Equations

• Lean.PersistentHashSet.insert s a = { set := Lean.PersistentHashMap.insert s.set a () }

@[inline]

def Lean.PersistentHashSet.erase {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Lean.PersistentHashSet α

Equations

• Lean.PersistentHashSet.erase s a = { set := Lean.PersistentHashMap.erase s.set a }

@[inline]

def Lean.PersistentHashSet.find? {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Option α

Equations

• Lean.PersistentHashSet.find? s a = match Lean.PersistentHashMap.findEntry? s.set a with | some (a, snd) => some a | none => none

@[inline]

def Lean.PersistentHashSet.contains {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → α → Bool

Equations

• Lean.PersistentHashSet.contains s a = Lean.PersistentHashMap.contains s.set a

@[inline]

def Lean.PersistentHashSet.size {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → Nat

Equations

• Lean.PersistentHashSet.size s = s.set.size

@[inline]

def Lean.PersistentHashSet.foldM {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → {m : Type v → Type v} → [inst : Monad m] → (β → α → m β) → β → Lean.PersistentHashSet α → m β

Equations

• Lean.PersistentHashSet.foldM f init s = Lean.PersistentHashMap.foldlM s.set (fun (d : β) (a : α) (x : Unit) => f d a) init

@[inline]

def Lean.PersistentHashSet.fold {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (β → α → β) → β → Lean.PersistentHashSet α → β

Equations

• Lean.PersistentHashSet.fold f init s = Id.run (Lean.PersistentHashSet.foldM f init s)