@[implicit_reducible]

def Std.DTreeMap.instCoeTypeForall_1 {α : Type u} : Coe (Type v) (α → Type v)

structure Std.DTreeMap.Raw (α : Type u) (β : α → Type v) (_cmp : α → α → Ordering := by exact compare) : Type (max u v)

Dependent tree maps 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 DTreeMap over DTreeMap.Raw. Lemmas about the operations on Std.DTreeMap.Raw are available in the module Std.Data.DTreeMap.Raw.Lemmas.

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. The get operations of the dependent tree map additionally require a LawfulEqCmp instance to ensure that cmp a b = .eq always implies a = b, so that their respective value types are equal.

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.

• inner : Internal.Impl α β

  Internal implementation detail of the tree map.

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

Well-formedness predicate for tree maps. Users of DTreeMap will not need to interact with this. Users of DTreeMap.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 map 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.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instCoeWFWFInner {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Raw α β cmp} : Coe t.WF t.inner.WF

@[inline]

def Std.DTreeMap.Raw.empty {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Raw α β 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 ∅.

@[implicit_reducible]

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

@[implicit_reducible]

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

structure Std.DTreeMap.Raw.Equiv {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (m₁ m₂ : Raw α β cmp) : Prop

Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.

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

  Internal implementation detail of the tree map

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

Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.

@[simp]

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

@[inline]

def Std.DTreeMap.Raw.insert {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (a : α) (b : β a) : Raw α β 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.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instSingletonSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Singleton ((a : α) × β a) (Raw α β cmp)

@[implicit_reducible]

instance Std.DTreeMap.Raw.instInsertSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Insert ((a : α) × β a) (Raw α β cmp)

instance Std.DTreeMap.Raw.instLawfulSingletonSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : LawfulSingleton ((a : α) × β a) (Raw α β cmp)

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.containsThenInsert {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (a : α) (b : β a) : Bool × Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.containsThenInsertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (a : α) (b : β a) : Bool × Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.getThenInsertIfNew? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (b : β a) : Option (β a) × Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.contains {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[implicit_reducible]

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

@[implicit_reducible]

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

@[inline]

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

Returns the number of mappings present in the map.

@[inline]

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

Returns true if the tree map contains no mappings.

@[inline]

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

Removes the mapping for the given key if it exists.

@[inline]

def Std.DTreeMap.Raw.get? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) : Option (β a)

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.

@[inline]

def Std.DTreeMap.Raw.get {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : β a

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.

@[inline]

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

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.

@[inline]

def Std.DTreeMap.Raw.getD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (fallback : β a) : β a

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.

@[inline]

def Std.DTreeMap.Raw.getEntry? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (a : α) : Option ((a : α) × β a)

Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise none. The key in the returned pair will be BEq to the input a.

@[inline]

def Std.DTreeMap.Raw.getEntry {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (h : a ∈ t) : (a : α) × β a

Retrieves the key-value pair, whose key matches a. Ensures that such a mapping exists by requiring a proof of a ∈ m. The key in the returned pair will be BEq to the input a.

@[inline]

def Std.DTreeMap.Raw.getEntry! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited ((a : α) × β a)] (t : Raw α β cmp) (a : α) : (a : α) × β a

Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics. The key in the returned pair will be BEq to the input a.

@[inline]

def Std.DTreeMap.Raw.getEntryD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (a : α) (fallback : (a : α) × β a) : (a : α) × β a

Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise fallback. The key in the returned pair will compare equal to the input a.

@[inline]

def Std.DTreeMap.Raw.getKey? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.getKey {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.getKey! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited α] (t : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.getKeyD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.minEntry? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) : Option ((a : α) × β a)

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

We do not provide minEntry for the raw trees.

@[inline]

def Std.DTreeMap.Raw.minEntry! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a

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

@[inline]

def Std.DTreeMap.Raw.minEntryD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a

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

@[inline]

def Std.DTreeMap.Raw.maxEntry? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) : Option ((a : α) × β a)

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

We do not provide maxEntry for the raw trees.

@[inline]

def Std.DTreeMap.Raw.maxEntry! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Inhabited ((a : α) × β a)] (t : Raw α β cmp) : (a : α) × β a

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

@[inline]

def Std.DTreeMap.Raw.maxEntryD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β cmp) (fallback : (a : α) × β a) : (a : α) × β a

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

@[inline]

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

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

We do not provide minKey for the raw trees.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

We do not provide maxKey for the raw trees.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

We do not provide entryAtIdx for the raw trees.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

We do not provide keyAtIdx for the raw trees.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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.

@[inline]

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

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.

@[inline]

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

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.

@[inline]

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

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

We do not provide getEntryGE, getEntryGT, getEntryLE, getEntryLT for the raw trees.

@[inline]

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

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.

@[inline]

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

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

@[inline]

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

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.

@[inline]

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

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

@[inline]

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

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.

@[inline]

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

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.

@[inline]

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

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.

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.getKeyGE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.getKeyLE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

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

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

We do not provide getKeyGE, getKeyGT, getKeyLE, getKeyLT for the raw trees.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.getKeyGED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.getKeyLED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Raw α β 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.

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.Const.getThenInsertIfNew? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (a : α) (b : β) : Option β × Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.get? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.get {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.get! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited β] (t : Raw α (fun (x : α) => β) cmp) (a : α) : β

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.

@[inline]

def Std.DTreeMap.Raw.Const.getD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.minEntry? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : Option (α × β)

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

We do not provide minEntry for the raw trees.

@[inline]

def Std.DTreeMap.Raw.Const.minEntry! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) cmp) : α × β

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

@[inline]

def Std.DTreeMap.Raw.Const.minEntryD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.maxEntry? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : Option (α × β)

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

@[inline]

def Std.DTreeMap.Raw.Const.maxEntry! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) cmp) : α × β

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

@[inline]

def Std.DTreeMap.Raw.Const.maxEntryD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.entryAtIdx? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (n : Nat) : Option (α × β)

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

We do not provide entryAtIdx for the raw trees.

@[inline]

def Std.DTreeMap.Raw.Const.entryAtIdx! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) cmp) (n : Nat) : α × β

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

@[inline]

def Std.DTreeMap.Raw.Const.entryAtIdxD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (n : Nat) (fallback : α × β) : α × β

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

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGE? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGT? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLE? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLT? {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (k : α) : Option (α × β)

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

We do not provide getEntryGE, getEntryGT, getEntryLE, getEntryLT for the raw trees.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGE! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGT! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLE! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLT! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Inhabited (α × β)] (t : Raw α (fun (x : α) => β) cmp) (k : α) : α × β

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

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGED {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryGTD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLED {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.getEntryLTD {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (k : α) (fallback : α × β) : α × β

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

@[inline]

def Std.DTreeMap.Raw.filter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (f : (a : α) → β a → Bool) (t : Raw α β cmp) : Raw α β cmp

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[implicit_reducible]

instance Std.DTreeMap.Raw.instForMSigmaOfMonad {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m] : ForM m (Raw α β cmp) ((a : α) × β a)

@[implicit_reducible]

instance Std.DTreeMap.Raw.instForInSigmaOfMonad {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m] : ForIn m (Raw α β cmp) ((a : α) × β a)

We do not define ForM and ForIn instances that are specialized to constant β. Instead, we define uncurried versions of forM and forIn that will be used in the Const lemmas and to define the ForM and ForIn instances for DTreeMap.Raw.

@[inline]

def Std.DTreeMap.Raw.Const.forMUncurried {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [Monad m] {β : Type v} (f : α × β → m PUnit) (t : Raw α (fun (x : α) => β) cmp) : m PUnit

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

@[inline]

def Std.DTreeMap.Raw.Const.forInUncurried {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [Monad m] {β : Type v} (f : α × β → δ → m (ForInStep δ)) (init : δ) (t : Raw α (fun (x : α) => β) cmp) : m δ

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.values {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : List β

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

@[inline]

def Std.DTreeMap.Raw.valuesArray {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : Array β

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

@[inline]

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

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

@[inline]

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

Transforms a list of mappings into a tree map.

@[inline]

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

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

@[inline]

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

Transforms an array of mappings into a tree map.

@[inline]

def Std.DTreeMap.Raw.modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (f : β a → β a) : Raw α β cmp

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

@[inline]

def Std.DTreeMap.Raw.alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (t : Raw α β cmp) (a : α) (f : Option (β a) → Option (β a)) : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.mergeWith {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : Raw α β cmp) : Raw α β 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.

@[inline]

def Std.DTreeMap.Raw.Const.toList {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : List (α × β)

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

@[inline]

def Std.DTreeMap.Raw.Const.ofList {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering := by exact compare) : Raw α (fun (x : α) => β) cmp

Transforms a list of mappings into a tree map.

@[inline]

def Std.DTreeMap.Raw.Const.unitOfList {α : Type u} (l : List α) (cmp : α → α → Ordering := by exact compare) : Raw α (fun (x : α) => Unit) cmp

Transforms a list of keys into a tree map.

@[inline]

def Std.DTreeMap.Raw.Const.toArray {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) : Array (α × β)

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

@[inline]

def Std.DTreeMap.Raw.Const.ofArray {α : Type u} {β : Type v} (a : Array (α × β)) (cmp : α → α → Ordering := by exact compare) : Raw α (fun (x : α) => β) cmp

Transforms a list of mappings into a tree map.

@[inline]

def Std.DTreeMap.Raw.Const.unitOfArray {α : Type u} (a : Array α) (cmp : α → α → Ordering := by exact compare) : Raw α (fun (x : α) => Unit) cmp

Transforms a list of mappings into a tree map.

@[inline]

def Std.DTreeMap.Raw.Const.modify {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (a : α) (f : β → β) : Raw α (fun (x : α) => β) cmp

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

@[inline]

def Std.DTreeMap.Raw.Const.alter {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t : Raw α (fun (x : α) => β) cmp) (a : α) (f : Option β → Option β) : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.mergeWith {α : Type u} {cmp : α → α → Ordering} {β : Type v} (mergeFn : α → β → β → β) (t₁ t₂ : Raw α (fun (x : α) => β) cmp) : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.insertMany {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ ((a : α) × β a)] (t : Raw α β cmp) (l : ρ) : Raw α β 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.

def Std.DTreeMap.Raw.union {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t₁ t₂ : Raw α β cmp) : Raw α β cmp

Computes the union of the given tree maps. If a key appears in both maps, the entry contained in the second argument will appear in the result.

This function always merges the smaller map into the larger map.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instUnion {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Union (Raw α β cmp)

def Std.DTreeMap.Raw.inter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t₁ t₂ : Raw α β cmp) : Raw α β cmp

Computes the intersection of the given tree maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instInter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : Inter (Raw α β cmp)

def Std.DTreeMap.Raw.beq {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] [(k : α) → BEq (β k)] (t₁ t₂ : Raw α β cmp) : Bool

Compares two tree maps using Boolean equality on keys and values.

Returns true if the maps contain the same key-value pairs, false otherwise.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instBEqOfLawfulEqCmp {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [LawfulEqCmp cmp] [(k : α) → BEq (β k)] : BEq (Raw α β cmp)

def Std.DTreeMap.Raw.Const.beq {α : Type u} {cmp : α → α → Ordering} {β : Type v} [BEq β] (t₁ t₂ : Raw α (fun (x : α) => β) cmp) : Bool

Compares two tree maps using Boolean equality on keys and values.

Returns true if the maps contain the same key-value pairs, false otherwise.

def Std.DTreeMap.Raw.diff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t₁ t₂ : Raw α β cmp) : Raw α β cmp

Computes the difference of the given tree maps. This function always iterates through the smaller map.

@[implicit_reducible]

instance Std.DTreeMap.Raw.instSDiff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : SDiff (Raw α β cmp)

@[inline]

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

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

@[inline]

def Std.DTreeMap.Raw.Const.insertMany {α : Type u} {cmp : α → α → Ordering} {β : Type v} {ρ : Type u_1} [ForIn Id ρ (α × β)] (t : Raw α (fun (x : α) => β) cmp) (l : ρ) : Raw α (fun (x : α) => β) 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.

@[inline]

def Std.DTreeMap.Raw.Const.insertManyIfNewUnit {α : Type u} {cmp : α → α → Ordering} {ρ : Type u_1} [ForIn Id ρ α] (t : Raw α (fun (x : α) => Unit) cmp) (l : ρ) : Raw α (fun (x : α) => 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.

@[implicit_reducible]

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