@[implicit_reducible]

instance Lean.PersistentHashSet.instForInOfMonad_batteries {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} [Monad m] : ForIn m (PersistentHashSet α) α

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

def Lean.PersistentHashSet.anyM {α : Type u_1} [BEq α] [Hashable α] {m : Type → Type u_2} [Monad m] (s : PersistentHashSet α) (f : α → m Bool) : 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} [BEq α] [Hashable α] (s : PersistentHashSet α) (f : α → Bool) : Bool

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

Equations

• s.any f = (s.anyM f).run

@[specialize #[]]

def Lean.PersistentHashSet.allM {α : Type u_1} [BEq α] [Hashable α] {m : Type → Type u_2} [Monad m] (s : PersistentHashSet α) (f : α → m Bool) : 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} [BEq α] [Hashable α] (s : PersistentHashSet α) (f : α → Bool) : Bool

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

Equations

• s.all f = (s.allM f).run

@[implicit_reducible]

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

Equations

• Lean.PersistentHashSet.instBEq_batteries = { beq := fun (s t : Lean.PersistentHashSet α) => (s.all fun (x : α) => t.contains x) && t.all fun (x : α) => s.contains x }

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

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} [BEq α] [Hashable α] (as : Array α) : PersistentHashSet α

Obtain a PersistentHashSet from an array.

Equations

• Lean.PersistentHashSet.ofArray as = Lean.PersistentHashSet.empty.insertMany as

@[inline]

def Lean.PersistentHashSet.ofList {α : Type u_1} [BEq α] [Hashable α] (as : List α) : PersistentHashSet α

Obtain a PersistentHashSet from a list.

Equations

• Lean.PersistentHashSet.ofList as = Lean.PersistentHashSet.empty.insertMany as

@[inline]

def Lean.PersistentHashSet.merge {α : Type u_1} [BEq α] [Hashable α] (s t : PersistentHashSet α) : PersistentHashSet α

Merge two PersistentHashSets.

Equations

• s.merge t = s.insertMany t