structure Std.TreeSet.Raw (α : Type u) (cmp : α → α → Ordering := by exact compare) : Type u

Tree sets without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called Raw.WF. When in doubt, prefer TreeSet over TreeSet.Raw. Lemmas about the operations on Std.TreeSet.Raw are available in the module Std.Data.TreeSet.Raw.Lemmas.

A tree set stores elements of a certain type in a certain order. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

• If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).
• If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e only one of them can be contained in a single tree set at the same time.

To avoid expensive copies, users should make sure that the tree set is used linearly.

Internally, the tree sets are represented as size-bounded trees, a type of self-balancing binary search tree with efficient order statistic lookups.

• inner : TreeMap.Raw α Unit cmp

  Internal implementation detail of the tree set.

structure Std.TreeSet.Raw.WF {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Prop

Well-formedness predicate for tree sets. Users of TreeSet will not need to interact with this. Users of TreeSet.Raw will need to provide proofs of WF to lemmas and should use lemmas like WF.empty and WF.insert (which are always named exactly like the operations they are about) to show that set operations preserve well-formedness. The constructors of this type are internal implementation details and should not be accessed by users.

• out : t.inner.WF

  Internal implementation detail of the tree map.

instance Std.TreeSet.Raw.instCoeWFWFUnitInner {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} : Coe t.WF t.inner.WF

Equations

• Std.TreeSet.Raw.instCoeWFWFUnitInner = { coe := ⋯ }

@[inline]

def Std.TreeSet.Raw.empty {α : Type u} {cmp : α → α → Ordering} : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.empty = { inner := Std.TreeMap.Raw.empty }

instance Std.TreeSet.Raw.instEmptyCollection {α : Type u} {cmp : α → α → Ordering} : EmptyCollection (Raw α cmp)

Equations

• Std.TreeSet.Raw.instEmptyCollection = { emptyCollection := Std.TreeSet.Raw.empty }

instance Std.TreeSet.Raw.instInhabited {α : Type u} {cmp : α → α → Ordering} : Inhabited (Raw α cmp)

Equations

• Std.TreeSet.Raw.instInhabited = { default := ∅ }

@[simp]

theorem Std.TreeSet.Raw.empty_eq_emptyc {α : Type u} {cmp : α → α → Ordering} : empty = ∅

@[inline]

def Std.TreeSet.Raw.insert {α : Type u} {cmp : α → α → Ordering} (l : Raw α cmp) (a : α) : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• l.insert a = { inner := l.inner.insertIfNew a () }

instance Std.TreeSet.Raw.instSingleton {α : Type u} {cmp : α → α → Ordering} : Singleton α (Raw α cmp)

Equations

• Std.TreeSet.Raw.instSingleton = { singleton := fun (e : α) => ∅.insert e }

instance Std.TreeSet.Raw.instInsert {α : Type u} {cmp : α → α → Ordering} : Insert α (Raw α cmp)

Equations

• Std.TreeSet.Raw.instInsert = { insert := fun (e : α) (s : Std.TreeSet.Raw α cmp) => s.insert e }

instance Std.TreeSet.Raw.instLawfulSingleton {α : Type u} {cmp : α → α → Ordering} : LawfulSingleton α (Raw α cmp)

@[inline]

def Std.TreeSet.Raw.containsThenInsert {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (a : α) : Bool × Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.containsThenInsert a = ((t.inner.containsThenInsertIfNew a ()).fst, { inner := (t.inner.containsThenInsertIfNew a ()).snd })

@[inline]

def Std.TreeSet.Raw.contains {α : Type u} {cmp : α → α → Ordering} (l : Raw α cmp) (a : α) : Bool

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• l.contains a = l.inner.contains a

instance Std.TreeSet.Raw.instMembership {α : Type u} {cmp : α → α → Ordering} : Membership α (Raw α cmp)

Equations

• Std.TreeSet.Raw.instMembership = { mem := fun (t : Std.TreeSet.Raw α cmp) (a : α) => t.contains a = true }

instance Std.TreeSet.Raw.instDecidableMem {α : Type u} {cmp : α → α → Ordering} {t : Raw α cmp} {a : α} : Decidable (a ∈ t)

Equations

• Std.TreeSet.Raw.instDecidableMem = inferInstanceAs (Decidable (t.contains a = true))

@[inline]

def Std.TreeSet.Raw.size {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Nat

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.size = t.inner.size

@[inline]

def Std.TreeSet.Raw.isEmpty {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Bool

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.isEmpty = t.inner.isEmpty

@[inline]

def Std.TreeSet.Raw.erase {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (a : α) : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.erase a = { inner := t.inner.erase a }

@[inline]

def Std.TreeSet.Raw.get? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (a : α) : Option α

Checks if given key is contained and returns the key if it is, otherwise none. The result in the some case is guaranteed to be pointer equal to the key in the map.

Equations

• t.get? a = t.inner.getKey? a

@[inline]

def Std.TreeSet.Raw.get {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (a : α) (h : a ∈ t) : α

Retrieves the key from the set that matches a. Ensures that such a key exists by requiring a proof of a ∈ m. The result is guaranteed to be pointer equal to the key in the set.

Equations

• t.get a h = t.inner.getKey a h

@[inline]

def Std.TreeSet.Raw.get! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (a : α) : α

Checks if given key is contained and returns the key if it is, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the set.

Equations

• t.get! a = t.inner.getKey! a

@[inline]

def Std.TreeSet.Raw.getD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (a fallback : α) : α

Checks if given key is contained and returns the key if it is, otherwise fallback. If they key is contained the result is guaranteed to be pointer equal to the key in the set.

Equations

• t.getD a fallback = t.inner.getKeyD a fallback

@[inline]

def Std.TreeSet.Raw.min? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Option α

Tries to retrieve the smallest element of the tree set, returning none if the set is empty.

Equations

• t.min? = t.inner.minKey?

We do not provide min for the raw trees.

@[inline]

def Std.TreeSet.Raw.min! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) : α

Tries to retrieve the smallest element of the tree set, panicking if the set is empty.

Equations

• t.min! = t.inner.minKey!

@[inline]

def Std.TreeSet.Raw.minD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (fallback : α) : α

Tries to retrieve the smallest element of the tree set, returning fallback if the tree set is empty.

Equations

• t.minD fallback = t.inner.minKeyD fallback

@[inline]

def Std.TreeSet.Raw.max? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Option α

Tries to retrieve the largest element of the tree set, returning none if the set is empty.

Equations

• t.max? = t.inner.maxKey?

We do not provide max for the raw trees.

@[inline]

def Std.TreeSet.Raw.max! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) : α

Tries to retrieve the largest element of the tree set, panicking if the set is empty.

Equations

• t.max! = t.inner.maxKey!

@[inline]

def Std.TreeSet.Raw.maxD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (fallback : α) : α

Tries to retrieve the largest element of the tree set, returning fallback if the tree set is empty.

Equations

• t.maxD fallback = t.inner.maxKeyD fallback

@[inline]

def Std.TreeSet.Raw.atIdx? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (n : Nat) : Option α

Returns the n-th smallest element, or none if n is at least t.size.

Equations

• t.atIdx? n = t.inner.keyAtIndex? n

We do not provide entryAtIdx for the raw trees.

@[inline]

def Std.TreeSet.Raw.atIdx! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (n : Nat) : α

Returns the n-th smallest element, or panics if n is at least t.size.

Equations

• t.atIdx! n = t.inner.keyAtIndex! n

@[inline]

def Std.TreeSet.Raw.atIdxD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (n : Nat) (fallback : α) : α

Returns the n-th smallest element, or fallback if n is at least t.size.

Equations

• t.atIdxD n fallback = t.inner.keyAtIndexD n fallback

@[inline]

def Std.TreeSet.Raw.getGE? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k : α) : Option α

Tries to retrieve the smallest element that is greater than or equal to the given element, returning none if no such element exists.

Equations

• t.getGE? k = t.inner.getKeyGE? k

@[inline]

def Std.TreeSet.Raw.getGT? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k : α) : Option α

Tries to retrieve the smallest element that is greater than the given element, returning none if no such element exists.

Equations

• t.getGT? k = t.inner.getKeyGT? k

@[inline]

def Std.TreeSet.Raw.getLE? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k : α) : Option α

Tries to retrieve the largest element that is less than or equal to the given element, returning none if no such element exists.

Equations

• t.getLE? k = t.inner.getKeyLE? k

@[inline]

def Std.TreeSet.Raw.getLT? {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k : α) : Option α

Tries to retrieve the smallest element that is less than the given element, returning none if no such element exists.

Equations

• t.getLT? k = t.inner.getKeyLT? k

We do not provide getGE, getGT, getLE, getLT for the raw trees.

@[inline]

def Std.TreeSet.Raw.getGE! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (k : α) : α

Tries to retrieve the smallest element that is greater than or equal to the given element, panicking if no such element exists.

Equations

• t.getGE! k = t.inner.getKeyGE! k

@[inline]

def Std.TreeSet.Raw.getGT! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (k : α) : α

Tries to retrieve the smallest element that is greater than the given element, panicking if no such element exists.

Equations

• t.getGT! k = t.inner.getKeyGT! k

@[inline]

def Std.TreeSet.Raw.getLE! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (k : α) : α

Tries to retrieve the largest element that is less than or equal to the given element, panicking if no such element exists.

Equations

• t.getLE! k = t.inner.getKeyLE! k

@[inline]

def Std.TreeSet.Raw.getLT! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α cmp) (k : α) : α

Tries to retrieve the smallest element that is less than the given element, panicking if no such element exists.

Equations

• t.getLT! k = t.inner.getKeyLT! k

@[inline]

def Std.TreeSet.Raw.getGED {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k fallback : α) : α

Tries to retrieve the smallest element that is greater than or equal to the given element, returning fallback if no such element exists.

Equations

• t.getGED k fallback = t.inner.getKeyGED k fallback

@[inline]

def Std.TreeSet.Raw.getGTD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k fallback : α) : α

Tries to retrieve the smallest element that is greater than the given element, returning fallback if no such element exists.

Equations

• t.getGTD k fallback = t.inner.getKeyGTD k fallback

@[inline]

def Std.TreeSet.Raw.getLED {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k fallback : α) : α

Tries to retrieve the largest element that is less than or equal to the given element, returning fallback if no such element exists.

Equations

• t.getLED k fallback = t.inner.getKeyLED k fallback

@[inline]

def Std.TreeSet.Raw.getLTD {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (k fallback : α) : α

Tries to retrieve the smallest element that is less than the given element, returning fallback if no such element exists.

Equations

• t.getLTD k fallback = t.inner.getKeyLTD k fallback

@[inline]

def Std.TreeSet.Raw.filter {α : Type u} {cmp : α → α → Ordering} (f : α → Bool) (t : Raw α cmp) : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.filter f t = { inner := Std.TreeMap.Raw.filter (fun (a : α) (x : Unit) => f a) t.inner }

@[inline]

def Std.TreeSet.Raw.foldlM {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m] (f : δ → α → m δ) (init : δ) (t : Raw α cmp) : m δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.foldlM f init t = Std.TreeMap.Raw.foldlM (fun (c : δ) (a : α) (x : Unit) => f c a) init t.inner

@[inline, deprecated Std.TreeSet.Raw.foldlM (since := "2025-02-12")]

def Std.TreeSet.Raw.foldM {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m] (f : δ → α → m δ) (init : δ) (t : Raw α cmp) : m δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.foldM f init t = Std.TreeSet.Raw.foldlM f init t

@[inline]

def Std.TreeSet.Raw.foldl {α : Type u} {cmp : α → α → Ordering} {δ : Type w} (f : δ → α → δ) (init : δ) (t : Raw α cmp) : δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.foldl f init t = Std.TreeMap.Raw.foldl (fun (c : δ) (a : α) (x : Unit) => f c a) init t.inner

@[inline, deprecated Std.TreeSet.Raw.foldl (since := "2025-02-12")]

def Std.TreeSet.Raw.fold {α : Type u} {cmp : α → α → Ordering} {δ : Type w} (f : δ → α → δ) (init : δ) (t : Raw α cmp) : δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.fold f init t = Std.TreeSet.Raw.foldl f init t

@[inline]

def Std.TreeSet.Raw.foldrM {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m] (f : α → δ → m δ) (init : δ) (t : Raw α cmp) : m δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.foldrM f init t = Std.TreeMap.Raw.foldrM (fun (a : α) (x : Unit) (acc : δ) => f a acc) init t.inner

@[inline]

def Std.TreeSet.Raw.foldr {α : Type u} {cmp : α → α → Ordering} {δ : Type w} (f : α → δ → δ) (init : δ) (t : Raw α cmp) : δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.foldr f init t = Std.TreeMap.Raw.foldr (fun (a : α) (x : Unit) (acc : δ) => f a acc) init t.inner

@[inline, deprecated Std.TreeSet.Raw.foldr (since := "2025-02-12")]

def Std.TreeSet.Raw.revFold {α : Type u} {cmp : α → α → Ordering} {δ : Type w} (f : δ → α → δ) (init : δ) (t : Raw α cmp) : δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.revFold f init t = Std.TreeSet.Raw.foldr (fun (a : α) (acc : δ) => f acc a) init t

@[inline]

def Std.TreeSet.Raw.partition {α : Type u} {cmp : α → α → Ordering} (f : α → Bool) (t : Raw α cmp) : Raw α cmp × Raw α cmp

Partitions a tree set into two tree sets based on a predicate.

Equations

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

@[inline]

def Std.TreeSet.Raw.forM {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m] (f : α → m PUnit) (t : Raw α cmp) : m PUnit

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.forM f t = Std.TreeMap.Raw.forM (fun (a : α) (x : Unit) => f a) t.inner

@[inline]

def Std.TreeSet.Raw.forIn {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m] (f : α → δ → m (ForInStep δ)) (init : δ) (t : Raw α cmp) : m δ

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• Std.TreeSet.Raw.forIn f init t = Std.TreeMap.Raw.forIn (fun (a : α) (x : Unit) (c : δ) => f a c) init t.inner

instance Std.TreeSet.Raw.instForM {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} : ForM m (Raw α cmp) α

Equations

• Std.TreeSet.Raw.instForM = { forM := fun [Monad m] (t : Std.TreeSet.Raw α cmp) (f : α → m PUnit) => Std.TreeSet.Raw.forM f t }

instance Std.TreeSet.Raw.instForIn {α : Type u} {cmp : α → α → Ordering} {t : Type w → Type w} : ForIn t (Raw α cmp) α

Equations

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

@[inline]

def Std.TreeSet.Raw.any {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (p : α → Bool) : Bool

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.any p = t.inner.any fun (a : α) (x : Unit) => p a

@[inline]

def Std.TreeSet.Raw.all {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) (p : α → Bool) : Bool

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.all p = t.inner.all fun (a : α) (x : Unit) => p a

@[inline]

def Std.TreeSet.Raw.toList {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : List α

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.toList = Std.DTreeMap.Internal.Impl.foldr (fun (a : α) (x : Unit) (l : List α) => a :: l) ∅ t.inner.inner.inner

@[inline]

def Std.TreeSet.Raw.ofList {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) : Raw α cmp

Transforms a list into a tree set.

Equations

• Std.TreeSet.Raw.ofList l cmp = { inner := Std.TreeMap.Raw.unitOfList l cmp }

@[inline, deprecated Std.TreeSet.Raw.ofList (since := "2025-02-12")]

def Std.TreeSet.Raw.fromList {α : Type u} (l : List α) (cmp : α → α → Ordering) : Raw α cmp

Transforms a list into a tree set.

Equations

• Std.TreeSet.Raw.fromList l cmp = Std.TreeSet.Raw.ofList l cmp

@[inline]

def Std.TreeSet.Raw.toArray {α : Type u} {cmp : α → α → Ordering} (t : Raw α cmp) : Array α

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.toArray = Std.TreeSet.Raw.foldl (fun (acc : Array α) (k : α) => acc.push k) #[] t

@[inline]

def Std.TreeSet.Raw.ofArray {α : Type u} (a : Array α) (cmp : α → α → Ordering := by exact compare) : Raw α cmp

Transforms an array into a tree set.

Equations

• Std.TreeSet.Raw.ofArray a cmp = { inner := Std.TreeMap.Raw.unitOfArray a cmp }

@[inline, deprecated Std.TreeSet.Raw.ofArray (since := "2025-02-12")]

def Std.TreeSet.Raw.fromArray {α : Type u} (a : Array α) (cmp : α → α → Ordering) : Raw α cmp

Transforms an array into a tree set.

Equations

• Std.TreeSet.Raw.fromArray a cmp = Std.TreeSet.Raw.ofArray a cmp

@[inline]

def Std.TreeSet.Raw.merge {α : Type u} {cmp : α → α → Ordering} (t₁ t₂ : Raw α cmp) : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t₁.merge t₂ = { inner := Std.TreeMap.Raw.mergeWith (fun (x : α) (x x : Unit) => ()) t₁.inner t₂.inner }

@[inline]

def Std.TreeSet.Raw.insertMany {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : Raw α cmp) (l : ρ) : Raw α cmp

Inserts multiple elements into the tree set by iterating over the given collection and calling insert. If the same element (with respect to cmp) appears multiple times, the first occurrence takes precedence.

Note: this precedence behavior is true for TreeSet and TreeSet.Raw. The insertMany function on TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw behaves differently: it will prefer the last appearance.

Equations

• t.insertMany l = { inner := t.inner.insertManyIfNewUnit l }

@[inline]

def Std.TreeSet.Raw.eraseMany {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : Raw α cmp) (l : ρ) : Raw α cmp

Creates a new empty tree set. It is also possible and recommended to use the empty collection notations ∅ and {} to create an empty tree set. simp replaces empty with ∅.

Equations

• t.eraseMany l = { inner := t.inner.eraseMany l }

instance Std.TreeSet.Raw.instRepr {α : Type u} {cmp : α → α → Ordering} [Repr α] : Repr (Raw α cmp)

Equations

• Std.TreeSet.Raw.instRepr = { reprPrec := fun (m : Std.TreeSet.Raw α cmp) (prec : Nat) => Repr.addAppParen (Std.Format.text "TreeSet.Raw.ofList " ++ repr m.toList) prec }