ink

@[specialize #[]]

def Lean.HashSet.anyM {α : Type u_1} [inst : BEq α] [inst : Hashable α] {m : Type → Type} [inst : 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.

ink

@[inline]

def Lean.HashSet.any {α : Type u_1} [inst : BEq α] [inst : Hashable α] (s : Lean.HashSet α) (f : α → Bool) : Bool

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

Equations

• Lean.HashSet.any s f = Id.run (Lean.HashSet.anyM s f)

ink

@[specialize #[]]

def Lean.HashSet.allM {α : Type u_1} [inst : BEq α] [inst : Hashable α] {m : Type → Type} [inst : 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.

ink

@[inline]

def Lean.HashSet.all {α : Type u_1} [inst : BEq α] [inst : Hashable α] (s : Lean.HashSet α) (f : α → Bool) : Bool

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

Equations

• Lean.HashSet.all s f = Id.run (Lean.HashSet.allM s f)

ink

instance Lean.HashSet.instBEqHashSet {α : Type u_1} [inst : BEq α] [inst : Hashable α] : BEq (Lean.HashSet α)

Equations

• Lean.HashSet.instBEqHashSet = { beq := fun s t => (Lean.HashSet.all s fun x => Lean.HashSet.contains t x) && Lean.HashSet.all t fun x => Lean.HashSet.contains s x }

ink

@[inline]

def Lean.HashSet.insert' {α : Type u_1} [inst : BEq α] [inst : 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↦ b.

Equations

• Lean.HashSet.insert' s a = let oldSize := Lean.HashSet.size s; let s := Lean.HashSet.insert s a; (s, Lean.HashSet.size s == oldSize)

ink

@[inline]

def Lean.HashSet.ofArray {α : Type u_1} [inst : BEq α] [inst : Hashable α] (as : Array α) : Lean.HashSet α

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

Equations

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

ink

@[inline]

def Lean.HashSet.ofList {α : Type u_1} [inst : BEq α] [inst : Hashable α] (as : Array α) : Lean.HashSet α

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

Equations

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

ink

@[inline]

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

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

Equations

• Lean.HashSet.merge s t = Lean.HashSet.fold (fun s a => Lean.HashSet.insert s a) s t