Tree maps

This file develops the type Std.TreeMap of tree maps.

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

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

structure Std.TreeMap (α : Type u) (β : Type v) (cmp : α → α → Ordering := by exact compare) : Type (max u v)

Tree maps.

A tree map stores an assignment of keys to values. 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 entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present.

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

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

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

• inner : DTreeMap α (fun (x : α) => β) cmp

  Internal implementation detail of the tree map.

@[inline]

def Std.TreeMap.empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} : TreeMap α β cmp

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

Equations

• Std.TreeMap.empty = { inner := Std.DTreeMap.empty }

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

Equations

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

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

Equations

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

@[simp]

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

@[inline]

def Std.TreeMap.insert {α : Type u} {β : Type v} {cmp : α → α → Ordering} (l : TreeMap α β cmp) (a : α) (b : β) : TreeMap α β cmp

Inserts the given mapping into the map. If there is already a mapping for the given key, then both key and value will be replaced.

Equations

• l.insert a b = { inner := l.inner.insert a b }

instance Std.TreeMap.instSingletonProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Singleton (α × β) (TreeMap α β cmp)

Equations

• Std.TreeMap.instSingletonProd = { singleton := fun (e : α × β) => ∅.insert e.fst e.snd }

instance Std.TreeMap.instInsertProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} : Insert (α × β) (TreeMap α β cmp)

Equations

• Std.TreeMap.instInsertProd = { insert := fun (e : α × β) (s : Std.TreeMap α β cmp) => s.insert e.fst e.snd }

instance Std.TreeMap.instLawfulSingletonProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} : LawfulSingleton (α × β) (TreeMap α β cmp)

@[inline]

def Std.TreeMap.insertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (b : β) : TreeMap α β cmp

If there is no mapping for the given key, inserts the given mapping into the map. Otherwise, returns the map unaltered.

Equations

• t.insertIfNew a b = { inner := t.inner.insertIfNew a b }

@[inline]

def Std.TreeMap.containsThenInsert {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (b : β) : Bool × TreeMap α β cmp

Checks whether a key is present in a map and unconditionally inserts a value for the key.

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

Equations

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

@[inline]

def Std.TreeMap.containsThenInsertIfNew {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (b : β) : Bool × TreeMap α β cmp

Checks whether a key is present in a map and inserts a value for the key if it was not found. If the returned Bool is true, then the returned map is unaltered. If the Bool is false, then the returned map has a new value inserted.

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

Equations

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

@[inline]

def Std.TreeMap.getThenInsertIfNew? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (b : β) : Option β × TreeMap α β cmp

Checks whether a key is present in a map, returning the associated value, and inserts a value for the key if it was not found.

If the returned value is some v, then the returned map is unaltered. If it is none, then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling get? followed by insertIfNew.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.getThenInsertIfNew? a b = ((Std.DTreeMap.Const.getThenInsertIfNew? t.inner a b).fst, { inner := (Std.DTreeMap.Const.getThenInsertIfNew? t.inner a b).snd })

@[inline]

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

Returns true if there is a mapping for the given key a or a key that is equal to a according to the comparator cmp. 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 maps, both use the given comparator cmp.

Equations

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

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

Equations

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

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

Equations

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

@[inline]

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

Returns the number of mappings present in the map.

Equations

• t.size = t.inner.size

@[inline]

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

Returns true if the tree map contains no mappings.

Equations

• t.isEmpty = t.inner.isEmpty

@[inline]

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

Removes the mapping for the given key if it exists.

Equations

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

@[inline]

def Std.TreeMap.get? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) : Option β

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.get? a = Std.DTreeMap.Const.get? t.inner a

@[inline, deprecated Std.TreeMap.get? (since := "2025-02-12")]

def Std.TreeMap.find? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) : Option β

Tries to retrieve the mapping for the given key, returning none if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.find? a = t.get? a

@[inline]

def Std.TreeMap.get {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : β

Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.get a h = Std.DTreeMap.Const.get t.inner a h

@[inline]

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

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.get! a = Std.DTreeMap.Const.get! t.inner a

@[inline, deprecated Std.TreeMap.get! (since := "2025-02-12")]

def Std.TreeMap.find! {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) [Inhabited β] : β

Tries to retrieve the mapping for the given key, panicking if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.find! a = t.get! a

@[inline]

def Std.TreeMap.getD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.getD a fallback = Std.DTreeMap.Const.getD t.inner a fallback

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

def Std.TreeMap.findD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (fallback : β) : β

Tries to retrieve the mapping for the given key, returning fallback if no such mapping is present.

Uses the LawfulEqCmp instance to cast the retrieved value to the correct type.

Equations

• t.findD a fallback = t.getD a fallback

instance Std.TreeMap.instGetElem?Mem {α : Type u} {β : Type v} {cmp : α → α → Ordering} : GetElem? (TreeMap α β cmp) α β fun (m : TreeMap α β cmp) (a : α) => a ∈ m

Equations

• Std.TreeMap.instGetElem?Mem = GetElem?.mk (fun (m : Std.TreeMap α β cmp) (a : α) => m.get? a) fun [Inhabited β] (m : Std.TreeMap α β cmp) (a : α) => m.get! a

@[inline]

def Std.TreeMap.getKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) : Option α

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

Equations

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

@[inline]

def Std.TreeMap.getKey {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (h : a ∈ t) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (a : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise panics. If no panic occurs the result is guaranteed to be pointer equal to the key in the map.

Equations

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

@[inline]

def Std.TreeMap.getKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a fallback : α) : α

Checks if a mapping for the given key exists and returns the key if it does, otherwise fallback. If a mapping exists the result is guaranteed to be pointer equal to the key in the map.

Equations

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

@[inline]

def Std.TreeMap.min? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Option (α × β)

Tries to retrieve the key-value pair with the smallest key in the tree map, returning none if the map is empty.

Equations

• t.min? = Std.DTreeMap.Const.min? t.inner

@[inline]

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

Given a proof that the tree map is not empty, retrieves the key-value pair with the smallest key.

Equations

• t.min h = Std.DTreeMap.Const.min t.inner h

@[inline]

def Std.TreeMap.min! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) : α × β

Tries to retrieve the key-value pair with the smallest key in the tree map, panicking if the map is empty.

Equations

• t.min! = Std.DTreeMap.Const.min! t.inner

@[inline]

def Std.TreeMap.minD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key in the tree map, returning fallback if the tree map is empty.

Equations

• t.minD fallback = Std.DTreeMap.Const.minD t.inner fallback

@[inline]

def Std.TreeMap.max? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Option (α × β)

Tries to retrieve the key-value pair with the largest key in the tree map, returning none if the map is empty.

Equations

• t.max? = Std.DTreeMap.Const.max? t.inner

@[inline]

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

Given a proof that the tree map is not empty, retrieves the key-value pair with the largest key.

Equations

• t.max h = Std.DTreeMap.Const.max t.inner h

@[inline]

def Std.TreeMap.max! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) : α × β

Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is empty.

Equations

• t.max! = Std.DTreeMap.Const.max! t.inner

@[inline]

def Std.TreeMap.maxD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the largest key in the tree map, returning fallback if the tree map is empty.

Equations

• t.maxD fallback = Std.DTreeMap.Const.maxD t.inner fallback

@[inline]

def Std.TreeMap.minKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Option α

Tries to retrieve the smallest key in the tree map, returning none if the map is empty.

Equations

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

@[inline]

def Std.TreeMap.minKey {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (h : t.isEmpty = false) : α

Given a proof that the tree map is not empty, retrieves the smallest key.

Equations

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

@[inline]

def Std.TreeMap.minKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) : α

Tries to retrieve the smallest key in the tree map, panicking if the map is empty.

Equations

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

@[inline]

def Std.TreeMap.minKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (fallback : α) : α

Tries to retrieve the smallest key in the tree map, returning fallback if the tree map is empty.

Equations

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

@[inline]

def Std.TreeMap.maxKey? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Option α

Tries to retrieve the largest key in the tree map, returning none if the map is empty.

Equations

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

@[inline]

def Std.TreeMap.maxKey {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (h : t.isEmpty = false) : α

Given a proof that the tree map is not empty, retrieves the largest key.

Equations

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

@[inline]

def Std.TreeMap.maxKey! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) : α

Tries to retrieve the largest key in the tree map, panicking if the map is empty.

Equations

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

@[inline]

def Std.TreeMap.maxKeyD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (fallback : α) : α

Tries to retrieve the largest key in the tree map, returning fallback if the tree map is empty.

Equations

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

@[inline]

def Std.TreeMap.entryAtIdx? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) : Option (α × β)

Returns the key-value pair with the n-th smallest key, or none if n is at least t.size.

Equations

• t.entryAtIdx? n = Std.DTreeMap.Const.entryAtIdx? t.inner n

@[inline]

def Std.TreeMap.entryAtIdx {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) (h : n < t.size) : α × β

Returns the key-value pair with the n-th smallest key.

Equations

• t.entryAtIdx n h = Std.DTreeMap.Const.entryAtIdx t.inner n h

@[inline]

def Std.TreeMap.entryAtIdx! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) (n : Nat) : α × β

Returns the key-value pair with the n-th smallest key, or panics if n is at least t.size.

Equations

• t.entryAtIdx! n = Std.DTreeMap.Const.entryAtIdx! t.inner n

@[inline]

def Std.TreeMap.entryAtIdxD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) (fallback : α × β) : α × β

Returns the key-value pair with the n-th smallest key, or fallback if n is at least t.size.

Equations

• t.entryAtIdxD n fallback = Std.DTreeMap.Const.entryAtIdxD t.inner n fallback

@[inline]

def Std.TreeMap.keyAtIndex? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) : Option α

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

Equations

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

@[inline]

def Std.TreeMap.keyAtIndex {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) (h : n < t.size) : α

Returns the n-th smallest key.

Equations

• t.keyAtIndex n h = t.inner.keyAtIndex n h

@[inline]

def Std.TreeMap.keyAtIndex! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (n : Nat) : α

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

Equations

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

@[inline]

def Std.TreeMap.keyAtIndexD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (n : Nat) (fallback : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getEntryGE? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option (α × β)

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, returning none if no such pair exists.

Equations

• t.getEntryGE? k = Std.DTreeMap.Const.getEntryGE? t.inner k

@[inline]

def Std.TreeMap.getEntryGT? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option (α × β)

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, returning none if no such pair exists.

Equations

• t.getEntryGT? k = Std.DTreeMap.Const.getEntryGT? t.inner k

@[inline]

def Std.TreeMap.getEntryLE? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option (α × β)

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, returning none if no such pair exists.

Equations

• t.getEntryLE? k = Std.DTreeMap.Const.getEntryLE? t.inner k

@[inline]

def Std.TreeMap.getEntryLT? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option (α × β)

Tries to retrieve the key-value pair with the smallest key that is less than the given key, returning none if no such pair exists.

Equations

• t.getEntryLT? k = Std.DTreeMap.Const.getEntryLT? t.inner k

getEntryGE, getEntryGT, getEntryLE, getEntryLT can be found in Std.Data.TreeMap.AdditionalOperations.

@[inline]

def Std.TreeMap.getEntryGE! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) (k : α) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, panicking if no such pair exists.

Equations

• t.getEntryGE! k = Std.DTreeMap.Const.getEntryGE! t.inner k

@[inline]

def Std.TreeMap.getEntryGT! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) (k : α) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, panicking if no such pair exists.

Equations

• t.getEntryGT! k = Std.DTreeMap.Const.getEntryGT! t.inner k

@[inline]

def Std.TreeMap.getEntryLE! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) (k : α) : α × β

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, panicking if no such pair exists.

Equations

• t.getEntryLE! k = Std.DTreeMap.Const.getEntryLE! t.inner k

@[inline]

def Std.TreeMap.getEntryLT! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited (α × β)] (t : TreeMap α β cmp) (k : α) : α × β

Tries to retrieve the key-value pair with the smallest key that is less than the given key, panicking if no such pair exists.

Equations

• t.getEntryLT! k = Std.DTreeMap.Const.getEntryLT! t.inner k

@[inline]

def Std.TreeMap.getEntryGED {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the given key, returning fallback if no such pair exists.

Equations

• t.getEntryGED k fallback = Std.DTreeMap.Const.getEntryGED t.inner k fallback

@[inline]

def Std.TreeMap.getEntryGTD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key that is greater than the given key, returning fallback if no such pair exists.

Equations

• t.getEntryGTD k fallback = Std.DTreeMap.Const.getEntryGTD t.inner k fallback

@[inline]

def Std.TreeMap.getEntryLED {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the largest key that is less than or equal to the given key, returning fallback if no such pair exists.

Equations

• t.getEntryLED k fallback = Std.DTreeMap.Const.getEntryLED t.inner k fallback

@[inline]

def Std.TreeMap.getEntryLTD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) (fallback : α × β) : α × β

Tries to retrieve the key-value pair with the smallest key that is less than the given key, returning fallback if no such pair exists.

Equations

• t.getEntryLTD k fallback = Std.DTreeMap.Const.getEntryLTD t.inner k fallback

@[inline]

def Std.TreeMap.getKeyGE? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyGT? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLE? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLT? {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k : α) : Option α

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

Equations

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

getKeyGE, getKeyGT, getKeyLE, getKeyLT can be found in Std.Data.TreeMap.AdditionalOperations.

@[inline]

def Std.TreeMap.getKeyGE! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (k : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyGT! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (k : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLE! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (k : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLT! {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Inhabited α] (t : TreeMap α β cmp) (k : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyGED {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k fallback : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyGTD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k fallback : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLED {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k fallback : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.getKeyLTD {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (k fallback : α) : α

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

Equations

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

@[inline]

def Std.TreeMap.filter {α : Type u} {β : Type v} {cmp : α → α → Ordering} (f : α → β → Bool) (m : TreeMap α β cmp) : TreeMap α β cmp

Removes all mappings of the map for which the given function returns false.

Equations

• Std.TreeMap.filter f m = { inner := Std.DTreeMap.filter f m.inner }

@[inline]

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

Folds the given monadic function over the mappings in the map in ascending order.

Equations

• Std.TreeMap.foldlM f init t = Std.DTreeMap.foldlM f init t.inner

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

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

Folds the given monadic function over the mappings in the map in ascending order.

Equations

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

@[inline]

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

Folds the given function over the mappings in the map in ascending order.

Equations

• Std.TreeMap.foldl f init t = Std.DTreeMap.foldl f init t.inner

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

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

Folds the given function over the mappings in the map in ascending order.

Equations

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

@[inline]

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

Folds the given monadic function over the mappings in the map in descending order.

Equations

• Std.TreeMap.foldrM f init t = Std.DTreeMap.foldrM f init t.inner

@[inline]

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

Folds the given function over the mappings in the map in descending order.

Equations

• Std.TreeMap.foldr f init t = Std.DTreeMap.foldr f init t.inner

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

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

Folds the given function over the mappings in the map in descending order.

Equations

• Std.TreeMap.revFold f init t = Std.TreeMap.foldr (fun (k : α) (v : β) (acc : δ) => f acc k v) init t

@[inline]

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

Partitions a tree map into two tree maps based on a predicate.

Equations

• Std.TreeMap.partition f t = ({ inner := (Std.DTreeMap.partition f t.inner).fst }, { inner := (Std.DTreeMap.partition f t.inner).snd })

@[inline]

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

Carries out a monadic action on each mapping in the tree map in ascending order.

Equations

• Std.TreeMap.forM f t = Std.DTreeMap.forM f t.inner

@[inline]

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

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

Equations

• Std.TreeMap.forIn f init t = Std.DTreeMap.forIn (fun (a : α) (b : β) (c : δ) => f a b c) init t.inner

instance Std.TreeMap.instForMProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} : ForM m (TreeMap α β cmp) (α × β)

Equations

• Std.TreeMap.instForMProd = { forM := fun [Monad m] (t : Std.TreeMap α β cmp) (f : α × β → m PUnit) => Std.TreeMap.forM (fun (a : α) (b : β) => f (a, b)) t }

instance Std.TreeMap.instForInProd {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} : ForIn m (TreeMap α β cmp) (α × β)

Equations

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

@[inline]

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

Check if any element satisfes the predicate, short-circuiting if a predicate fails.

Equations

• t.any p = t.inner.any p

@[inline]

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

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

Equations

• t.all p = t.inner.all p

@[inline]

def Std.TreeMap.keys {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : List α

Returns a list of all keys present in the tree map in ascending order.

Equations

• t.keys = t.inner.keys

@[inline]

def Std.TreeMap.keysArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Array α

Returns an array of all keys present in the tree map in ascending order.

Equations

• t.keysArray = t.inner.keysArray

@[inline]

def Std.TreeMap.values {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : List β

Returns a list of all values present in the tree map in ascending order.

Equations

• t.values = t.inner.values

@[inline]

def Std.TreeMap.valuesArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Array β

Returns an array of all values present in the tree map in ascending order.

Equations

• t.valuesArray = t.inner.valuesArray

@[inline]

def Std.TreeMap.toList {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : List (α × β)

Transforms the tree map into a list of mappings in ascending order.

Equations

• t.toList = Std.DTreeMap.Const.toList t.inner

@[inline]

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

Transforms a list of mappings into a tree map.

Equations

• Std.TreeMap.ofList l cmp = { inner := Std.DTreeMap.Const.ofList l cmp }

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

def Std.TreeMap.fromList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : TreeMap α β cmp

Transforms a list of mappings into a tree map.

Equations

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

@[inline]

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

Transforms a list of keys into a tree map.

Equations

• Std.TreeMap.unitOfList l cmp = { inner := Std.DTreeMap.Const.unitOfList l cmp }

@[inline]

def Std.TreeMap.toArray {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) : Array (α × β)

Transforms the tree map into a list of mappings in ascending order.

Equations

• t.toArray = Std.DTreeMap.Const.toArray t.inner

@[inline]

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

Transforms a list of mappings into a tree map.

Equations

• Std.TreeMap.ofArray a cmp = { inner := Std.DTreeMap.Const.ofArray a cmp }

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

def Std.TreeMap.fromArray {α : Type u} {β : Type v} (a : Array (α × β)) (cmp : α → α → Ordering) : TreeMap α β cmp

Transforms a list of mappings into a tree map.

Equations

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

@[inline]

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

Transforms an array of keys into a tree map.

Equations

• Std.TreeMap.unitOfArray a cmp = { inner := Std.DTreeMap.Const.unitOfArray a cmp }

@[inline]

def Std.TreeMap.modify {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (f : β → β) : TreeMap α β cmp

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

Equations

• t.modify a f = { inner := Std.DTreeMap.Const.modify t.inner a f }

@[inline]

def Std.TreeMap.alter {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t : TreeMap α β cmp) (a : α) (f : Option β → Option β) : TreeMap α β cmp

Modifies in place the value associated with a given key, allowing creating new values and deleting values via an Option valued replacement function.

This function ensures that the value is used linearly.

Equations

• t.alter a f = { inner := Std.DTreeMap.Const.alter t.inner a f }

@[inline]

def Std.TreeMap.mergeWith {α : Type u} {β : Type v} {cmp : α → α → Ordering} (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

This function ensures that t₁ is used linearly. It also uses the individual values in t₁ linearly if the merge function uses the second argument (i.e. the first of type β a) 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₁ if t₁ does not contain a conflicting mapping yet. If t₁ does contain a conflicting mapping, use the given merge function to merge the mapping in t₂ into the mapping in t₁. Then return 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

• Std.TreeMap.mergeWith mergeFn t₁ t₂ = { inner := Std.DTreeMap.Const.mergeWith mergeFn t₁.inner t₂.inner }

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

def Std.TreeMap.mergeBy {α : Type u} {β : Type v} {cmp : α → α → Ordering} (mergeFn : α → β → β → β) (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp

Returns a map that contains all mappings of t₁ and t₂. In case that both maps contain the same key k with respect to cmp, the provided function is used to determine the new value from the respective values in t₁ and t₂.

This function ensures that t₁ is used linearly. It also uses the individual values in t₁ linearly if the merge function uses the second argument (i.e. the first of type β a) 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₁ if t₁ does not contain a conflicting mapping yet. If t₁ does contain a conflicting mapping, use the given merge function to merge the mapping in t₂ into the mapping in t₁. Then return 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

• Std.TreeMap.mergeBy mergeFn t₁ t₂ = Std.TreeMap.mergeWith mergeFn t₁ t₂

@[inline]

def Std.TreeMap.insertMany {α : Type u} {β : Type v} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ (α × β)] (t : TreeMap α β cmp) (l : ρ) : TreeMap α β cmp

Inserts multiple mappings into the tree map by iterating over the given collection and calling insert. If the same key appears multiple times, the last occurrence takes precedence.

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

Equations

• t.insertMany l = { inner := Std.DTreeMap.Const.insertMany t.inner l }

@[inline]

def Std.TreeMap.insertManyIfNewUnit {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : TreeMap α Unit cmp) (l : ρ) : TreeMap α Unit cmp

Inserts multiple elements into the tree map by iterating over the given collection and calling insertIfNew. If the same key appears multiple times, the first occurrence takes precedence.

Equations

• t.insertManyIfNewUnit l = { inner := Std.DTreeMap.Const.insertManyIfNewUnit t.inner l }

@[inline]

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

Erases multiple mappings from the tree map by iterating over the given collection and calling erase.

Equations

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

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

Equations

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