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

- set : PersistentHashMap α Unit

Instances For

source
@[reducible, inline]
abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] :
Type u
Equations

- Lean.PHashSet α = Lean.PersistentHashSet α

Instances For

source
@[inline]
def Lean.PersistentHashSet.empty {α : Type u_1} [BEq α] [Hashable α] :
PersistentHashSet α
Equations

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

Instances For

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

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

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

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

source
@[inline]
def Lean.PersistentHashSet.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
Bool
Equations

- s.isEmpty = s.set.isEmpty

Instances For

source
@[inline]
def Lean.PersistentHashSet.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
PersistentHashSet α
Equations

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

Instances For

source
@[inline]
def Lean.PersistentHashSet.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
PersistentHashSet α
Equations

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

Instances For

source
@[inline]
def Lean.PersistentHashSet.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
Option α
Equations

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

Instances For

source
@[inline]
def Lean.PersistentHashSet.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
Bool
Equations

- s.contains a = s.set.contains a

Instances For

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

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

Instances For

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

- Lean.PersistentHashSet.fold f init s = (Lean.PersistentHashSet.foldM (fun (x1 : β) (x2 : α) => pure (f x1 x2)) init s).run

Instances For

source
def Lean.PersistentHashSet.toList {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
List α
Equations

- s.toList = List.map (fun (x : α × Unit) => x.fst) s.set.toList

Instances For

source
def Lean.PersistentHashSet.forIn {α : Type u_1} {m : Type u_2 → Type u_3} {σ : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] (s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) :
m σ
Equations

- s.forIn init f = s.set.forIn init fun (p : α × Unit) (s : σ) => f p.fst s

Instances For

source
instance Lean.PersistentHashSet.instForIn {α : Type u_1} {m : Type u_2 → Type u_3} {x✝ : BEq α} {x✝¹ : Hashable α} :
ForIn m (PersistentHashSet α) α
Equations

- Lean.PersistentHashSet.instForIn = { forIn := fun {β : Type ?u.25} [Monad m] => Lean.PersistentHashSet.forIn }