# Documentation

Std.Lean.HashSet

@[specialize #[]]
def Lean.HashSet.anyM {α : Type u_1} [inst : BEq α] [inst : ] {m : } [inst : ] (s : ) (f : αm Bool) :

O(n). Returns true if f returns true for any element of the set.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.HashSet.any {α : Type u_1} [inst : BEq α] [inst : ] (s : ) (f : αBool) :

O(n). Returns true if f returns true for any element of the set.

Equations
@[specialize #[]]
def Lean.HashSet.allM {α : Type u_1} [inst : BEq α] [inst : ] {m : } [inst : ] (s : ) (f : αm Bool) :

O(n). Returns true if f returns true for all elements of the set.

Equations
• One or more equations did not get rendered due to their size.
@[inline]
def Lean.HashSet.all {α : Type u_1} [inst : BEq α] [inst : ] (s : ) (f : αBool) :

O(n). Returns true if f returns true for all elements of the set.

Equations
instance Lean.HashSet.instBEqHashSet {α : Type u_1} [inst : BEq α] [inst : ] :
BEq ()
Equations
@[inline]
def Lean.HashSet.insert' {α : Type u_1} [inst : BEq α] [inst : ] (s : ) (a : α) :

O(1) amortized. Similar to insert, but also returns a Boolean flag indicating whether an existing entry has been replaced with a ↦ b↦ b.

Equations
• = let oldSize := ; let s := ; (s, == oldSize)
@[inline]
def Lean.HashSet.ofArray {α : Type u_1} [inst : BEq α] [inst : ] (as : ) :

O(n). Obtain a HashSet from an array.

Equations
@[inline]
def Lean.HashSet.ofList {α : Type u_1} [inst : BEq α] [inst : ] (as : ) :

O(n). Obtain a HashSet from a list.

Equations
@[inline]
def Lean.HashSet.merge {α : Type u} [inst : BEq α] [inst : ] (s : ) (t : ) :

O(|t|) amortized. Merge two HashSets.

Equations