source
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.

Instances For

source
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.

Instances For

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

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

source
@[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 }

Instances For

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

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

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

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

source
structure Std.TreeSet.Raw.Equiv {α : Type u} {cmp : α → α → Ordering} (m₁ m₂ : Raw α 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

Instances For

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

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

Equations

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

Instances For

source
@[simp]
theorem Std.TreeSet.Raw.empty_eq_emptyc {α : Type u} {cmp : α → α → Ordering} :
empty = ∅
source
@[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 () }

Instances For

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

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

source
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 }

source
instance Std.TreeSet.Raw.instLawfulSingleton {α : Type u} {cmp : α → α → Ordering} :
LawfulSingleton α (Raw α cmp)
source
@[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 })

Instances For

source
@[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

Instances For

source
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 }

source
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))

source
@[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

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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?

Instances For

We do not provide `min` for the raw trees.

source
@[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!

Instances For

source
@[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

Instances For

source
@[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?

Instances For

We do not provide `max` for the raw trees.

source
@[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!

Instances For

source
@[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

Instances For

source
@[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.keyAtIdx? n

Instances For

We do not provide `entryAtIdx` for the raw trees.

source
@[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.keyAtIdx! n

Instances For

source
@[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.keyAtIdxD n fallback

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

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

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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.

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
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 }

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

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

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

source
@[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_1 x_2 : Unit) => ()) t₁.inner t₂.inner }

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
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 "Std.TreeSet.Raw.ofList " ++ repr m.toList) prec }