Documentation

Std.Lean.HashSet

source
instance Lean.HashSet.instSingleton_std {α : Type u_1} [BEq α] [Hashable α] :
Singleton α (Lean.HashSet α)
Equations
  • Lean.HashSet.instSingleton_std = { singleton := fun (x : α) => Lean.HashSet.empty.insert x }
source
instance Lean.HashSet.instInsert_std {α : Type u_1} [BEq α] [Hashable α] :
Insert α (Lean.HashSet α)
Equations
  • Lean.HashSet.instInsert_std = { insert := fun (a : α) (s : Lean.HashSet α) => s.insert a }
source
@[specialize #[]]
def Lean.HashSet.anyM {α : Type u_1} [BEq α] [Hashable α] {m : Type → Type} [Monad m] (s : Lean.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.
source
@[inline]
def Lean.HashSet.any {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (f : α → Bool) :
Bool

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

Equations
  • s.any f = (s.anyM f).run
source
@[specialize #[]]
def Lean.HashSet.allM {α : Type u_1} [BEq α] [Hashable α] {m : Type → Type} [Monad m] (s : Lean.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.
source
@[inline]
def Lean.HashSet.all {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (f : α → Bool) :
Bool

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

Equations
  • s.all f = (s.allM f).run
source
instance Lean.HashSet.instBEq_std {α : Type u_1} [BEq α] [Hashable α] :
BEq (Lean.HashSet α)
Equations
  • Lean.HashSet.instBEq_std = { beq := fun (s t : Lean.HashSet α) => (s.all fun (x : α) => t.contains x) && t.all fun (x : α) => s.contains x }
source
@[inline]
def Lean.HashSet.insert' {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (a : α) :
Lean.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 = let oldSize := s.size; let s := s.insert a; (s, s.size == oldSize)
source
@[inline]
def Lean.HashSet.ofArray {α : Type u_1} [BEq α] [Hashable α] (as : Array α) :
Lean.HashSet α

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

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

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

Equations