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

- Std.DTreeMap.instCoeTypeForall_1 = { coe := fun (γ : Type ?u.10) (x : α) => γ }

Instances For

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

Instances For

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

Instances For

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

- Std.DTreeMap.Raw.instCoeWFWFInner = { coe := ⋯ }

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

Equations

- Std.DTreeMap.Raw.empty = { inner := Std.DTreeMap.Internal.Impl.empty }

Instances For

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

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

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

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

source
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

Instances For

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

Equations

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

Instances For

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

Equations

- t.insert a b = { inner := Std.DTreeMap.Internal.Impl.insert! a b t.inner }

Instances For

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

- Std.DTreeMap.Raw.instSingletonSigma = { singleton := fun (e : (a : α) × β a) => ∅.insert e.fst e.snd }

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

- Std.DTreeMap.Raw.instInsertSigma = { insert := fun (e : (a : α) × β a) (s : Std.DTreeMap.Raw α β cmp) => s.insert e.fst e.snd }

source
instance Std.DTreeMap.Raw.instLawfulSingletonSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} :
LawfulSingleton ((a : α) × β a) (Raw α β cmp)
source
@[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.

Equations

- t.insertIfNew a b = { inner := Std.DTreeMap.Internal.Impl.insertIfNew! a b t.inner }

Instances For

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

Equations

- t.containsThenInsert a b = ((Std.DTreeMap.Internal.Impl.containsThenInsert! a b t.inner).fst, { inner := (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t.inner).snd })

Instances For

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

Equations

- t.containsThenInsertIfNew a b = ((Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t.inner).fst, { inner := (Std.DTreeMap.Internal.Impl.containsThenInsertIfNew! a b t.inner).snd })

Instances For

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

Equations

- t.getThenInsertIfNew? a b = ((t.inner.getThenInsertIfNew?! a b).fst, { inner := (t.inner.getThenInsertIfNew?! a b).snd })

Instances For

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

Equations

- t.contains a = Std.DTreeMap.Internal.Impl.contains a t.inner

Instances For

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

- Std.DTreeMap.Raw.instMembership = { mem := fun (t : Std.DTreeMap.Raw α β cmp) (a : α) => t.contains a = true }

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

- Std.DTreeMap.Raw.instDecidableMem = inferInstanceAs (Decidable (t.contains a = true))

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

Equations

- t.size = t.inner.size

Instances For

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

Equations

- t.isEmpty = t.inner.isEmpty

Instances For

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

Equations

- t.erase a = { inner := Std.DTreeMap.Internal.Impl.erase! a t.inner }

Instances For

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

Equations

- t.get? a = t.inner.get? a

Instances For

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

Equations

- t.get a h = t.inner.get a h

Instances For

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

Equations

- t.get! a = t.inner.get! a

Instances For

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

Equations

- t.getD a fallback = t.inner.getD a fallback

Instances For

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

Equations

- t.getKey? a = t.inner.getKey? a

Instances For

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

Equations

- t.getKey a h = t.inner.getKey a h

Instances For

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

Equations

- t.getKey! a = t.inner.getKey! a

Instances For

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

Equations

- t.getKeyD a fallback = t.inner.getKeyD a fallback

Instances For

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

Equations

- t.minEntry? = t.inner.minEntry?

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.minEntry? (since := "2025-03-13")]
def Std.DTreeMap.Raw.min? {α : 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.

Equations

- t.min? = t.minEntry?

Instances For

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

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

Equations

- t.minEntry! = t.inner.minEntry!

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.minEntry! (since := "2025-03-13")]
def Std.DTreeMap.Raw.min! {α : 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.

Equations

- t.min! = t.minEntry!

Instances For

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

Equations

- t.minEntryD fallback = t.inner.minEntryD fallback

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.minEntryD (since := "2025-03-13")]
def Std.DTreeMap.Raw.minD {α : 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.

Equations

- t.minD fallback = t.minEntryD fallback

Instances For

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

Equations

- t.maxEntry? = t.inner.maxEntry?

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.maxEntry? (since := "2025-03-13")]
def Std.DTreeMap.Raw.max? {α : 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.

Equations

- t.max? = t.maxEntry?

Instances For

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

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

Equations

- t.maxEntry! = t.inner.maxEntry!

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.maxEntry! (since := "2025-03-13")]
def Std.DTreeMap.Raw.max! {α : 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.

Equations

- t.max! = t.maxEntry!

Instances For

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

Equations

- t.maxEntryD fallback = t.inner.maxEntryD fallback

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.maxEntryD (since := "2025-03-13")]
def Std.DTreeMap.Raw.maxD {α : 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.

Equations

- t.maxD fallback = t.maxEntryD fallback

Instances For

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

Equations

- t.minKey? = t.inner.minKey?

Instances For

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

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

Equations

- t.minKeyD fallback = t.inner.minKeyD fallback

Instances For

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

Equations

- t.minKey! = t.inner.minKey!

Instances For

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

Equations

- t.maxKey? = t.inner.maxKey?

Instances For

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

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

Equations

- t.maxKey! = t.inner.maxKey!

Instances For

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

Equations

- t.maxKeyD fallback = t.inner.maxKeyD fallback

Instances For

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

Equations

- t.entryAtIdx? n = t.inner.entryAtIdx? n

Instances For

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

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

Equations

- t.entryAtIdx! n = t.inner.entryAtIdx! n

Instances For

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

Equations

- t.entryAtIdxD n fallback = t.inner.entryAtIdxD n fallback

Instances For

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

Equations

- t.keyAtIdx? n = t.inner.keyAtIdx? n

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.keyAtIdx? (since := "2025-03-25")]
def Std.DTreeMap.Raw.keyAtIndex? {α : 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`.

Equations

- t.keyAtIndex? n = t.keyAtIdx? n

Instances For

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

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

Equations

- t.keyAtIdx! n = t.inner.keyAtIdx! n

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.keyAtIdx! (since := "2025-03-25")]
def Std.DTreeMap.Raw.keyAtIndex! {α : 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`.

Equations

- t.keyAtIndex! n = t.keyAtIdx! n

Instances For

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

Equations

- t.keyAtIdxD n fallback = t.inner.keyAtIdxD n fallback

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.keyAtIdxD (since := "2025-03-25")]
def Std.DTreeMap.Raw.keyAtIndexD {α : 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`.

Equations

- t.keyAtIndexD n fallback = t.keyAtIdxD n fallback

Instances For

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

Equations

- t.getEntryGE? k = Std.DTreeMap.Internal.Impl.getEntryGE? k t.inner

Instances For

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

Equations

- t.getEntryGT? k = Std.DTreeMap.Internal.Impl.getEntryGT? k t.inner

Instances For

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

Equations

- t.getEntryLE? k = Std.DTreeMap.Internal.Impl.getEntryLE? k t.inner

Instances For

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

Equations

- t.getEntryLT? k = Std.DTreeMap.Internal.Impl.getEntryLT? k t.inner

Instances For

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

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

Equations

- t.getEntryGE! k = Std.DTreeMap.Internal.Impl.getEntryGE! k t.inner

Instances For

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

Equations

- t.getEntryGT! k = Std.DTreeMap.Internal.Impl.getEntryGT! k t.inner

Instances For

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

Equations

- t.getEntryLE! k = Std.DTreeMap.Internal.Impl.getEntryLE! k t.inner

Instances For

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

Equations

- t.getEntryLT! k = Std.DTreeMap.Internal.Impl.getEntryLT! k t.inner

Instances For

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

Equations

- t.getEntryGED k fallback = Std.DTreeMap.Internal.Impl.getEntryGED k t.inner fallback

Instances For

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

Equations

- t.getEntryGTD k fallback = Std.DTreeMap.Internal.Impl.getEntryGTD k t.inner fallback

Instances For

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

Equations

- t.getEntryLED k fallback = Std.DTreeMap.Internal.Impl.getEntryLED k t.inner fallback

Instances For

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

Equations

- t.getEntryLTD k fallback = Std.DTreeMap.Internal.Impl.getEntryLTD k t.inner fallback

Instances For

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

Equations

- t.getKeyGE? k = Std.DTreeMap.Internal.Impl.getKeyGE? k t.inner

Instances For

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

Equations

- t.getKeyGT? k = Std.DTreeMap.Internal.Impl.getKeyGT? k t.inner

Instances For

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

Equations

- t.getKeyLE? k = Std.DTreeMap.Internal.Impl.getKeyLE? k t.inner

Instances For

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

Equations

- t.getKeyLT? k = Std.DTreeMap.Internal.Impl.getKeyLT? k t.inner

Instances For

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

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

Equations

- t.getKeyGE! k = Std.DTreeMap.Internal.Impl.getKeyGE! k t.inner

Instances For

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

Equations

- t.getKeyGT! k = Std.DTreeMap.Internal.Impl.getKeyGT! k t.inner

Instances For

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

Equations

- t.getKeyLE! k = Std.DTreeMap.Internal.Impl.getKeyLE! k t.inner

Instances For

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

Equations

- t.getKeyLT! k = Std.DTreeMap.Internal.Impl.getKeyLT! k t.inner

Instances For

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

Equations

- t.getKeyGED k fallback = Std.DTreeMap.Internal.Impl.getKeyGED k t.inner fallback

Instances For

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

Equations

- t.getKeyGTD k fallback = Std.DTreeMap.Internal.Impl.getKeyGTD k t.inner fallback

Instances For

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

Equations

- t.getKeyLED k fallback = Std.DTreeMap.Internal.Impl.getKeyLED k t.inner fallback

Instances For

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

Equations

- t.getKeyLTD k fallback = Std.DTreeMap.Internal.Impl.getKeyLTD k t.inner fallback

Instances For

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

Equations

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

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.get? t a = Std.DTreeMap.Internal.Impl.Const.get? t.inner a

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.get t a h = Std.DTreeMap.Internal.Impl.Const.get t.inner a h

Instances For

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

- Std.DTreeMap.Raw.Const.get! t a = Std.DTreeMap.Internal.Impl.Const.get! t.inner a

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getD t a fallback = Std.DTreeMap.Internal.Impl.Const.getD t.inner a fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.minEntry? t = Std.DTreeMap.Internal.Impl.Const.minEntry? t.inner

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.minEntry? (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.min? {α : 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.

Equations

- Std.DTreeMap.Raw.Const.min? t = Std.DTreeMap.Raw.Const.minEntry? t

Instances For

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

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

Equations

- Std.DTreeMap.Raw.Const.minEntry! t = Std.DTreeMap.Internal.Impl.Const.minEntry! t.inner

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.minEntry! (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.min! {α : 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.

Equations

- Std.DTreeMap.Raw.Const.min! t = Std.DTreeMap.Raw.Const.minEntry! t

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.minEntryD t fallback = Std.DTreeMap.Internal.Impl.Const.minEntryD t.inner fallback

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.minEntryD (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.minD {α : 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.

Equations

- Std.DTreeMap.Raw.Const.minD t fallback = Std.DTreeMap.Raw.Const.minEntryD t fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.maxEntry? t = Std.DTreeMap.Internal.Impl.Const.maxEntry? t.inner

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.maxEntry? (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.max? {α : 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.

Equations

- Std.DTreeMap.Raw.Const.max? t = Std.DTreeMap.Raw.Const.maxEntry? t

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.maxEntry! t = Std.DTreeMap.Internal.Impl.Const.maxEntry! t.inner

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.maxEntry! (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.max! {α : 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.

Equations

- Std.DTreeMap.Raw.Const.max! t = Std.DTreeMap.Raw.Const.maxEntry! t

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.maxEntryD t fallback = Std.DTreeMap.Internal.Impl.Const.maxEntryD t.inner fallback

Instances For

source
@[inline, deprecated Std.DTreeMap.Raw.Const.maxEntryD (since := "2025-03-13")]
def Std.DTreeMap.Raw.Const.maxD {α : 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.

Equations

- Std.DTreeMap.Raw.Const.maxD t fallback = Std.DTreeMap.Raw.Const.maxEntryD t fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.entryAtIdx? t n = Std.DTreeMap.Internal.Impl.Const.entryAtIdx? t.inner n

Instances For

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

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

Equations

- Std.DTreeMap.Raw.Const.entryAtIdx! t n = Std.DTreeMap.Internal.Impl.Const.entryAtIdx! t.inner n

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.entryAtIdxD t n fallback = Std.DTreeMap.Internal.Impl.Const.entryAtIdxD t.inner n fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGE? t k = Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGT? t k = Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLE? t k = Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLT? t k = Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t.inner

Instances For

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

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGE! t k = Std.DTreeMap.Internal.Impl.Const.getEntryGE! k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGT! t k = Std.DTreeMap.Internal.Impl.Const.getEntryGT! k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLE! t k = Std.DTreeMap.Internal.Impl.Const.getEntryLE! k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLT! t k = Std.DTreeMap.Internal.Impl.Const.getEntryLT! k t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGED t k fallback = Std.DTreeMap.Internal.Impl.Const.getEntryGED k t.inner fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryGTD t k fallback = Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t.inner fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLED t k fallback = Std.DTreeMap.Internal.Impl.Const.getEntryLED k t.inner fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.getEntryLTD t k fallback = Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t.inner fallback

Instances For

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

Equations

- Std.DTreeMap.Raw.filter f t = { inner := Std.DTreeMap.Internal.Impl.filter! f t.inner }

Instances For

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

Equations

- Std.DTreeMap.Raw.foldlM f init t = Std.DTreeMap.Internal.Impl.foldlM f init t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.foldl f init t = Std.DTreeMap.Internal.Impl.foldl f init t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.foldrM f init t = Std.DTreeMap.Internal.Impl.foldrM f init t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.foldr f init t = Std.DTreeMap.Internal.Impl.foldr f init t.inner

Instances For

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

Equations

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

Instances For

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

Equations

- Std.DTreeMap.Raw.forM f t = Std.DTreeMap.Internal.Impl.forM f t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.forIn f init t = Std.DTreeMap.Internal.Impl.forIn f init t.inner

Instances For

source
instance Std.DTreeMap.Raw.instForMSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} :
ForM m (Raw α β cmp) ((a : α) × β a)
Equations

- Std.DTreeMap.Raw.instForMSigma = { forM := fun [Monad m] (t : Std.DTreeMap.Raw α β cmp) (f : (a : α) × β a → m PUnit) => Std.DTreeMap.Raw.forM (fun (a : α) (b : β a) => f ⟨a, b⟩) t }

source
instance Std.DTreeMap.Raw.instForInSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} :
ForIn m (Raw α β cmp) ((a : α) × β a)
Equations

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

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

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

Equations

- Std.DTreeMap.Raw.Const.forMUncurried f t = Std.DTreeMap.Internal.Impl.forM (fun (a : α) (b : β) => f (a, b)) t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.forInUncurried f init t = Std.DTreeMap.Internal.Impl.forIn (fun (a : α) (b : β) (d : δ) => f (a, b) d) init t.inner

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

- t.keys = t.inner.keys

Instances For

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

Equations

- t.keysArray = t.inner.keysArray

Instances For

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

Equations

- t.values = t.inner.values

Instances For

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

Equations

- t.valuesArray = t.inner.valuesArray

Instances For

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

Equations

- t.toList = t.inner.toList

Instances For

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

Equations

- Std.DTreeMap.Raw.ofList l cmp = { inner := Std.DTreeMap.Internal.Impl.ofList l }

Instances For

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

Equations

- t.toArray = t.inner.toArray

Instances For

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

Equations

- Std.DTreeMap.Raw.ofArray a cmp = { inner := Std.DTreeMap.Internal.Impl.ofArray a }

Instances For

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

Equations

- t.modify a f = { inner := Std.DTreeMap.Internal.Impl.modify a f t.inner }

Instances For

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

Equations

- t.alter a f = { inner := Std.DTreeMap.Internal.Impl.alter! a f t.inner }

Instances For

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

Equations

- Std.DTreeMap.Raw.mergeWith mergeFn t₁ t₂ = { inner := Std.DTreeMap.Internal.Impl.mergeWith! mergeFn t₁.inner t₂.inner }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.toList t = Std.DTreeMap.Internal.Impl.Const.toList t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.ofList l cmp = { inner := Std.DTreeMap.Internal.Impl.Const.ofList l }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.unitOfList l cmp = { inner := Std.DTreeMap.Internal.Impl.Const.unitOfList l }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.toArray t = Std.DTreeMap.Internal.Impl.Const.toArray t.inner

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.ofArray a cmp = { inner := Std.DTreeMap.Internal.Impl.Const.ofArray a }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.unitOfArray a cmp = { inner := Std.DTreeMap.Internal.Impl.Const.unitOfArray a }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.modify t a f = { inner := Std.DTreeMap.Internal.Impl.Const.modify a f t.inner }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.alter t a f = { inner := Std.DTreeMap.Internal.Impl.Const.alter! a f t.inner }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.mergeWith mergeFn t₁ t₂ = { inner := Std.DTreeMap.Internal.Impl.Const.mergeWith! mergeFn t₁.inner t₂.inner }

Instances For

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

Equations

- t.insertMany l = { inner := (t.inner.insertMany! l).val }

Instances For

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

Equations

- t.eraseMany l = { inner := (t.inner.eraseMany! l).val }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.insertMany t l = { inner := (Std.DTreeMap.Internal.Impl.Const.insertMany! t.inner l).val }

Instances For

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

Equations

- Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l = { inner := (Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t.inner l).val }

Instances For

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

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