Extensional tree sets

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

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

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

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

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

In contrast to regular dependent tree maps, Std.ExtTreeSet offers several extensionality lemmas and therefore has more lemmas about equality of tree sets. This doesn't affect the amount of supported functions though: Std.ExtTreeSet supports all operations from Std.TreeMap.

In order to use most functions, a TransCmp instance is required. This is necessary to make sure that the functions are congruent, i.e. equivalent tree sets as parameters produce equivalent return values.

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 ExtTreeSet over TreeSet.Raw.

• inner : ExtTreeMap α Unit cmp

  Internal implementation detail of the tree map.

@[inline]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[inline]

def Std.ExtTreeSet.insert {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (l : ExtTreeSet α cmp) (a : α) : ExtTreeSet α 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 ExtTreeSet and ExtTreeSet.Raw. The insert function on ExtTreeMap, ExtDTreeMap, ExtTreeMap.Raw and ExtDTreeMap.Raw behaves differently: it will overwrite an existing mapping.

Equations

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

instance Std.ExtTreeSet.instSingletonOfTransCmp {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : Singleton α (ExtTreeSet α cmp)

Equations

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

instance Std.ExtTreeSet.instInsertOfTransCmp {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : Insert α (ExtTreeSet α cmp)

Equations

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

instance Std.ExtTreeSet.instLawfulSingleton {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : LawfulSingleton α (ExtTreeSet α cmp)

@[inline]

def Std.ExtTreeSet.containsThenInsert {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) : Bool × ExtTreeSet α 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.ExtTreeSet.contains {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (l : ExtTreeSet α 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.ExtTreeSet.instMembershipOfTransCmp {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] : Membership α (ExtTreeSet α cmp)

Equations

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

instance Std.ExtTreeSet.instDecidableMem {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {m : ExtTreeSet α cmp} {a : α} : Decidable (a ∈ m)

Equations

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

@[inline]

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

Returns the number of mappings present in the map.

Equations

• t.size = t.inner.size

@[inline]

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

Returns true if the tree set contains no mappings.

Equations

• t.isEmpty = t.inner.isEmpty

@[inline]

def Std.ExtTreeSet.erase {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (a : α) : ExtTreeSet α cmp

Removes the given key if it exists.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Std.ExtTreeSet.max! {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α 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.ExtTreeSet.maxD {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.atIdx? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.atIdx {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.atIdx! {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtTreeSet α 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.ExtTreeSet.atIdxD {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.getGE? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.getGT? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.getLE? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.getLT? {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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

@[inline]

def Std.ExtTreeSet.getGE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isGE = true) : α

Given a proof that such an element exists, retrieves the smallest element that is greater than or equal to the given element.

Equations

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

@[inline]

def Std.ExtTreeSet.getGT {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : α

Given a proof that such an element exists, retrieves the smallest element that is greater than the given element.

Equations

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

@[inline]

def Std.ExtTreeSet.getLE {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : α

Given a proof that such an element exists, retrieves the largest element that is less than or equal to the given element.

Equations

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

@[inline]

def Std.ExtTreeSet.getLT {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : α

Given a proof that such an element exists, retrieves the smallest element that is less than the given element.

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

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

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

Equations

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

@[inline]

def Std.ExtTreeSet.partition {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (f : α → Bool) (t : ExtTreeSet α cmp) : ExtTreeSet α cmp × ExtTreeSet α 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.ExtTreeSet.forM {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m] [LawfulMonad m] [TransCmp cmp] (f : α → m PUnit) (t : ExtTreeSet α cmp) : m PUnit

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

Equations

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

@[inline]

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

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

Equations

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

instance Std.ExtTreeSet.instForMOfTransCmpOfLawfulMonad {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtTreeSet α cmp) α

Equations

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

instance Std.ExtTreeSet.instForInOfTransCmpOfLawfulMonad {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtTreeSet α cmp) α

Equations

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

@[inline]

def Std.ExtTreeSet.any {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.all {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α 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.ExtTreeSet.toList {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) : List α

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

Equations

• t.toList = t.inner.keys

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

Transforms a list into a tree set.

Equations

• Std.ExtTreeSet.ofList l cmp = { inner := Std.ExtTreeMap.unitOfList l cmp }

@[inline]

def Std.ExtTreeSet.toArray {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtTreeSet α cmp) : Array α

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

Equations

• t.toArray = t.inner.keysArray

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

Transforms an array into a tree set.

Equations

• Std.ExtTreeSet.ofArray a cmp = { inner := Std.ExtTreeMap.unitOfArray a cmp }

@[inline]

def Std.ExtTreeSet.merge {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] (t₁ t₂ : ExtTreeSet α cmp) : ExtTreeSet α 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.ExtTreeMap.mergeWith (fun (x : α) (x x : Unit) => ()) t₁.inner t₂.inner }

@[inline]

def Std.ExtTreeSet.insertMany {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {ρ : Type u_1} [ForIn Id ρ α] (t : ExtTreeSet α cmp) (l : ρ) : ExtTreeSet α 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 ExtTreeSet and ExtTreeSet.Raw. The insertMany function on ExtTreeMap, ExtDTreeMap, ExtTreeMap.Raw and ExtDTreeMap.Raw behaves differently: it will prefer the last appearance.

Equations

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

@[inline]

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

Equations

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