instance Std.HashSet.instSingleton_batteries {α : Type u_1} [BEq α] [Hashable α] : Singleton α (Std.HashSet α)

Equations

• Std.HashSet.instSingleton_batteries = { singleton := fun (x : α) => Std.HashSet.empty.insert x }

instance Std.HashSet.instInsert_batteries {α : Type u_1} [BEq α] [Hashable α] : Insert α (Std.HashSet α)

Equations

• Std.HashSet.instInsert_batteries = { insert := fun (a : α) (s : Std.HashSet α) => s.insert a }

@[specialize #[]]

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

@[specialize #[]]

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

instance Std.HashSet.instBEq_batteries {α : Type u_1} [BEq α] [Hashable α] : BEq (Std.HashSet α)

Equations

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

@[inline, deprecated Std.HashSet.containsThenInsert]

def Std.HashSet.insert' {α : Type u_1} [BEq α] [Hashable α] (s : Std.HashSet α) (a : α) : Std.HashSet α × Bool

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

Equations

• s.insert' a = (s.insert a, (s.insert a).size == s.size)