Documentation

Std.Lean.PersistentHashSet

instance Lean.PersistentHashSet.instForInPersistentHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] {m : Type u_2 → Type u_3} :
Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.PersistentHashSet.anyM {α : Type u_1} [inst : BEq α] [inst : Hashable α] {m : TypeType u_2} [inst : Monad m] (s : Lean.PersistentHashSet α) (f : αm Bool) :

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.PersistentHashSet.any {α : Type u_1} [inst : BEq α] [inst : Hashable α] (s : Lean.PersistentHashSet α) (f : αBool) :

Returns true if f returns true for any element of the set.

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

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.PersistentHashSet.all {α : Type u_1} [inst : BEq α] [inst : Hashable α] (s : Lean.PersistentHashSet α) (f : αBool) :

Returns true if f returns true for all elements of the set.

Equations
Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Lean.PersistentHashSet.insert' {α : Type u_1} [inst : BEq α] [inst : Hashable α] (s : Lean.PersistentHashSet α) (a : α) :

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

Equations
def Lean.PersistentHashSet.insertMany {α : Type u_1} [inst : BEq α] [inst : Hashable α] {ρ : Type u_2} [inst : ForIn Id ρ α] (s : Lean.PersistentHashSet α) (as : ρ) :

Insert all elements from a collection into a PersistentHashSet.

Equations
  • One or more equations did not get rendered due to their size.
@[inline]
def Lean.PersistentHashSet.ofArray {α : Type u_1} [inst : BEq α] [inst : Hashable α] (as : Array α) :

Obtain a PersistentHashSet from an array.

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

Obtain a PersistentHashSet from a list.

Equations
@[inline]

Merge two PersistentHashSets.

Equations