Tree sets

This file develops the type Std.TreeSet of tree sets.

Lemmas about the operations on Std.Data.TreeSet will be available in the module Std.Data.TreeSet.Lemmas.

See the module Std.Data.TreeSet.Raw.Basic for a variant of this type which is safe to use in nested inductive types and Std.Data.ExtTreeSet.Basic for a variant with extensionality.

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

Tree sets.

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., there can be only one of them 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.

For use in proofs, the type Std.ExtTreeSet of extensional tree sets should be preferred. This type comes with several extensionality lemmas and provides the same functions but requires a TransCmp instance to work with.

These tree sets contain a bundled well-formedness invariant, which means that they cannot be used in nested inductive types. For these use cases, Std.TreeSet.Raw and Std.TreeSet.Raw.WF unbundle the invariant from the tree set. When in doubt, prefer TreeSet over TreeSet.Raw.

• inner : TreeMap α Unit cmp

  Internal implementation detail of the tree map.

@[inline]

def Std.TreeSet.empty {α : Type u} {cmp : α → α → Ordering} : TreeSet α 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.empty = { inner := Std.TreeMap.empty }

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

Equations

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

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

Equations

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

structure Std.TreeSet.Equiv {α : Type u} {cmp : α → α → Ordering} (m₁ m₂ : TreeSet α cmp) : Prop

Two tree sets are equivalent in the sense of Equiv iff all the values are equal.

• inner : m₁.inner.Equiv m₂.inner

  Internal implementation detail of the tree map

def Std.TreeSet.«term_~m_» : Lean.TrailingParserDescr

Two tree sets are equivalent in the sense of Equiv iff all the values are equal.

Equations

• Std.TreeSet.«term_~m_» = Lean.ParserDescr.trailingNode `Std.TreeSet.«term_~m_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ~m ") (Lean.ParserDescr.cat `term 51))

@[simp]

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

@[inline]

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

Inserts the given element into the set. If the tree set already contains an element that is equal (with regard to cmp) to the given element, then the tree set is returned unchanged.

Note: this non-replacement behavior is true for TreeSet and TreeSet.Raw. The insert function on TreeMap, DTreeMap, TreeMap.Raw and DTreeMap.Raw behaves differently: it will overwrite an existing mapping.

Equations

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

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

Equations

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

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

Equations

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

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

@[inline]

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

Checks whether an element is present in a set and inserts the element if it was not found. If the tree set already contains an element that is equal (with regard to cmp to the given element, then the tree set is returned unchanged.

Equivalent to (but potentially faster than) calling contains followed by insert.

Equations

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

@[inline]

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

Returns true if a, or an element equal to a according to the comparator cmp, is contained in the set. There is also a Prop-valued version of this: a ∈ t is equivalent to t.contains a = true.

Observe that this is different behavior than for lists: for lists, ∈ uses = and contains uses == for equality checks, while for tree sets, both use the given comparator cmp.

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Returns the number of mappings present in the map.

Equations

• t.size = t.inner.size

@[inline]

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

Returns true if the tree set contains no mappings.

Equations

• t.isEmpty = t.inner.isEmpty

@[inline]

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

Removes the given key if it exists.

Equations

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

@[inline]

def Std.TreeSet.get? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.get {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.get! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.getD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.min? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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?

@[inline]

def Std.TreeSet.min {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α cmp) (h : t.isEmpty = false) : α

Given a proof that the tree set is not empty, retrieves the smallest element.

Equations

• t.min h = t.inner.minKey h

@[inline]

def Std.TreeSet.min! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.minD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.max? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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?

@[inline]

def Std.TreeSet.max {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α cmp) (h : t.isEmpty = false) : α

Given a proof that the tree set is not empty, retrieves the largest element.

Equations

• t.max h = t.inner.maxKey h

@[inline]

def Std.TreeSet.max! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.maxD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.atIdx? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.keyAtIdx? n

@[inline]

def Std.TreeSet.atIdx {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α cmp) (n : Nat) (h : n < t.size) : α

Returns the n-th smallest element.

Equations

• t.atIdx n h = t.inner.keyAtIdx n h

@[inline]

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

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

Equations

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

@[inline]

def Std.TreeSet.atIdxD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.keyAtIdxD n fallback

@[inline]

def Std.TreeSet.getGE? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getGT? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getLE? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getLT? {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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

getGE, getGT, getLE, getLT can be found in Std.Data.TreeSet.AdditionalOperations.

@[inline]

def Std.TreeSet.getGE! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.getGT! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.getLE! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.getLT! {α : Type u} {cmp : α → α → Ordering} [Inhabited α] (t : TreeSet α 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.getGED {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getGTD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getLED {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.getLTD {α : Type u} {cmp : α → α → Ordering} (t : TreeSet α 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.filter {α : Type u} {cmp : α → α → Ordering} (f : α → Bool) (m : TreeSet α cmp) : TreeSet α cmp

Removes all elements from the tree set for which the given function returns false.

Equations

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

@[inline]

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

Monadically computes a value by folding the given function over the elements in the tree set in ascending order.

Equations

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

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

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

Monadically computes a value by folding the given function over the elements in the tree set in ascending order.

Equations

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

@[inline]

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

Folds the given function over the elements of the tree set in ascending order.

Equations

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

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

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

Folds the given function over the elements of the tree set in ascending order.

Equations

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

@[inline]

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

Monadically computes a value by folding the given function over the elements in the tree set in descending order.

Equations

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

@[inline]

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

Folds the given function over the elements of the tree set in descending order.

Equations

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

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

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

Folds the given function over the elements of the tree set in descending order.

Equations

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

@[inline]

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

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

Equations

• Std.TreeSet.partition f t = ({ inner := (Std.TreeMap.partition (fun (a : α) (x : Unit) => f a) t.inner).fst }, { inner := (Std.TreeMap.partition (fun (a : α) (x : Unit) => f a) t.inner).snd })

@[inline]

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

Carries out a monadic action on each element in the tree set in ascending order.

Equations

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

@[inline]

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

Support for the for loop construct in do blocks. The iteration happens in ascending order.

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Check if all elements satisfy the predicate, short-circuiting if a predicate fails.

Equations

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

@[inline]

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

Check if any element satisfies the predicate, short-circuiting if a predicate succeeds.

Equations

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

@[inline]

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

Transforms the tree set into a list of elements in ascending order.

Equations

• t.toList = t.inner.keys

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

Transforms a list into a tree set.

Equations

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

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

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

Transforms a list into a tree set.

Equations

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

@[inline]

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

Transforms the tree set into an array of elements in ascending order.

Equations

• t.toArray = t.inner.keysArray

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

Transforms an array into a tree set.

Equations

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

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

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

Transforms an array into a tree set.

Equations

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

@[inline]

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

Returns a set that contains all mappings of t₁ and `t₂.

This function ensures that t₁ is used linearly. Hence, as long as t₁ is unshared, the performance characteristics follow the following imperative description: Iterate over all mappings in t₂, inserting them into t₁.

Hence, the runtime of this method scales logarithmically in the size of t₁ and linearly in the size of t₂ as long as t₁ is unshared.

Equations

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

@[inline]

def Std.TreeSet.insertMany {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : TreeSet α cmp) (l : ρ) : TreeSet α 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.eraseMany {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : TreeSet α cmp) (l : ρ) : TreeSet α cmp

Erases multiple items from the tree set by iterating over the given collection and calling erase.

Equations

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

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

Equations

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