ink

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

Equations

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

ink

@[specialize #[]]

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

ink

@[inline]

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

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

Equations

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

ink

@[specialize #[]]

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

ink

@[inline]

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

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

Equations

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

ink

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

Equations

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

ink

@[inline]

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

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

Equations

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

ink

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

Insert all elements from a collection into a PersistentHashSet.

Equations

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

ink

@[inline]

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

Obtain a PersistentHashSet from an array.

Equations

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

ink

@[inline]

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

Obtain a PersistentHashSet from a list.

Equations

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

ink

@[inline]

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

Merge two PersistentHashSets.

Equations

• Lean.PersistentHashSet.merge s t = Lean.PersistentHashSet.insertMany s t