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

• set : Lean.PersistentHashMap α Unit

@[reducible, inline]

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.instInhabited {α : Type u_1} [BEq α] [Hashable α] : Inhabited (Lean.PersistentHashSet α)

Equations

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

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

Equations

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

@[inline]

def Lean.PersistentHashSet.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : Lean.PersistentHashSet α) : Bool

Equations

• s.isEmpty = s.set.isEmpty

@[inline]

def Lean.PersistentHashSet.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : Lean.PersistentHashSet α) (a : α) : Lean.PersistentHashSet α

Equations

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

@[inline]

def Lean.PersistentHashSet.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : Lean.PersistentHashSet α) (a : α) : Lean.PersistentHashSet α

Equations

• s.erase a = { set := s.set.erase a }

@[inline]

def Lean.PersistentHashSet.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : Lean.PersistentHashSet α) (a : α) : Option α

Equations

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

@[inline]

def Lean.PersistentHashSet.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : Lean.PersistentHashSet α) (a : α) : Bool

Equations

• s.contains a = s.set.contains a

@[inline]

def Lean.PersistentHashSet.foldM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Type v → Type v} [Monad m] (f : β → α → m β) (init : β) (s : Lean.PersistentHashSet α) : m β

Equations

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

@[inline]

def Lean.PersistentHashSet.fold {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (f : β → α → β) (init : β) (s : Lean.PersistentHashSet α) : β

Equations

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