Extensional dependent tree maps

This file develops the type Std.ExtDTreeMap of extensional dependent tree maps.

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

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

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

Extensional dependent tree maps.

A tree map stores an assignment of keys to values. It depends on a comparator function that defines an ordering on the keys and provides efficient order-dependent queries, such as retrieval of the minimum or maximum.

To ensure that the operations behave as expected, the comparator function cmp should satisfy certain laws that ensure a consistent ordering:

• If a is less than (or equal) to b, then b is greater than (or equal) to a and vice versa (see the OrientedCmp typeclass).
• If a is less than or equal to b and b is, in turn, less than or equal to c, then a is less than or equal to c (see the TransCmp typeclass).

Keys for which cmp a b = Ordering.eq are considered the same, i.e., there can be only one entry with key either a or b in a tree map. Looking up either a or b always yields the same entry, if any is present. 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.

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

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

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

• mk' :: (
• inner : Quotient (DTreeMap.isSetoid α β cmp)

  Implementation detail of the tree map

• )

@[reducible, inline]

abbrev Std.ExtDTreeMap.mk {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : DTreeMap α β cmp) : ExtDTreeMap α β cmp

Implementation detail of the tree map

Equations

• Std.ExtDTreeMap.mk t = { inner := Quotient.mk (Std.DTreeMap.isSetoid α β cmp) t }

@[reducible, inline]

abbrev Std.ExtDTreeMap.lift {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {γ : Sort w} (f : DTreeMap α β cmp → γ) (h : ∀ (a b : DTreeMap α β cmp), a.Equiv b → f a = f b) (t : ExtDTreeMap α β cmp) : γ

Implementation detail of the tree map

Equations

• Std.ExtDTreeMap.lift f h t = Quotient.lift f h t.inner

@[reducible, inline]

abbrev Std.ExtDTreeMap.liftOn₂ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {γ : Sort w} (t₁ t₂ : ExtDTreeMap α β cmp) (f : DTreeMap α β cmp → DTreeMap α β cmp → γ) (h : ∀ (a b c d : DTreeMap α β cmp), a.Equiv c → b.Equiv d → f a b = f c d) : γ

Implementation detail of the tree map

Equations

• t₁.liftOn₂ t₂ f h = t₁.inner.liftOn₂ t₂.inner f h

@[reducible, inline]

abbrev Std.ExtDTreeMap.pliftOn {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {γ : Sort w} (t : ExtDTreeMap α β cmp) (f : (x : DTreeMap α β cmp) → t = mk x → γ) (h : ∀ (a b : DTreeMap α β cmp) (h₁ : t = mk a) (h₂ : t = mk b), a.Equiv b → f a h₁ = f b h₂) : γ

Implementation detail of the tree map

Equations

• t.pliftOn f h = t.inner.pliftOn (fun (x : Std.DTreeMap α β cmp) (hx : t.inner = Quotient.mk (Std.DTreeMap.isSetoid α β cmp) x) => f x ⋯) ⋯

theorem Std.ExtDTreeMap.sound {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} (h : t₁.Equiv t₂) : mk t₁ = mk t₂

theorem Std.ExtDTreeMap.exact {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : DTreeMap α β cmp} (h : mk t₁ = mk t₂) : t₁.Equiv t₂

theorem Std.ExtDTreeMap.inductionOn {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {motive : ExtDTreeMap α β cmp → Prop} (t : ExtDTreeMap α β cmp) (mk : ∀ (a : DTreeMap α β cmp), motive (mk a)) : motive t

theorem Std.ExtDTreeMap.inductionOn₂ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {motive : ExtDTreeMap α β cmp → ExtDTreeMap α β cmp → Prop} (t₁ t₂ : ExtDTreeMap α β cmp) (mk : ∀ (a b : DTreeMap α β cmp), motive (mk a) (mk b)) : motive t₁ t₂

@[inline]

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

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

Equations

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

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

Equations

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

@[simp]

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

@[inline]

def Std.ExtDTreeMap.insert {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (b : β a) : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (m.insert a b)) ⋯ t

instance Std.ExtDTreeMap.instSingletonSigmaOfTransCmp {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] : Singleton ((a : α) × β a) (ExtDTreeMap α β cmp)

Equations

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

instance Std.ExtDTreeMap.instInsertSigmaOfTransCmp {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] : Insert ((a : α) × β a) (ExtDTreeMap α β cmp)

Equations

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

instance Std.ExtDTreeMap.instLawfulSingletonSigma {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] : LawfulSingleton ((a : α) × β a) (ExtDTreeMap α β cmp)

@[inline]

def Std.ExtDTreeMap.insertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (b : β a) : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (m.insertIfNew a b)) ⋯ t

@[inline]

def Std.ExtDTreeMap.containsThenInsert {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (b : β a) : Bool × ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => have m' := m.containsThenInsert a b; (m'.fst, Std.ExtDTreeMap.mk m'.snd)) ⋯ t

@[inline]

def Std.ExtDTreeMap.containsThenInsertIfNew {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (b : β a) : Bool × ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => have m' := m.containsThenInsertIfNew a b; (m'.fst, Std.ExtDTreeMap.mk m'.snd)) ⋯ t

@[inline]

def Std.ExtDTreeMap.getThenInsertIfNew? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (b : β a) : Option (β a) × ExtDTreeMap α β cmp

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

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

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

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

Equations

• t.getThenInsertIfNew? a b = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => have m' := m.getThenInsertIfNew? a b; (m'.fst, Std.ExtDTreeMap.mk m'.snd)) ⋯ t

@[inline]

def Std.ExtDTreeMap.contains {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.contains a) ⋯ t

instance Std.ExtDTreeMap.instMembershipOfTransCmp {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] : Membership α (ExtDTreeMap α β cmp)

Equations

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

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

Equations

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

@[inline]

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

Returns the number of mappings present in the map.

Equations

• t.size = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.size) ⋯ t

@[inline]

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

Returns true if the tree map contains no mappings.

Equations

• t.isEmpty = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.isEmpty) ⋯ t

@[simp]

theorem Std.ExtDTreeMap.isEmpty_iff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : ExtDTreeMap α β cmp} [TransCmp cmp] : t.isEmpty = true ↔ t = ∅

@[simp]

theorem Std.ExtDTreeMap.isEmpty_eq_false_iff {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : ExtDTreeMap α β cmp} [TransCmp cmp] : t.isEmpty = false ↔ ¬t = ∅

@[inline]

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

Removes the mapping for the given key if it exists.

Equations

• t.erase a = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (m.erase a)) ⋯ t

@[inline]

def Std.ExtDTreeMap.get? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.get? a) ⋯ t

@[inline]

def Std.ExtDTreeMap.get {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β 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.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.get a ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.get! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.get! a) ⋯ t

@[inline]

def Std.ExtDTreeMap.getD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getD a fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKey? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKey? a) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKey {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getKey a ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.getKey! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKey! a) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyD a fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.minEntry? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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? = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minEntry?) ⋯ t

@[inline]

def Std.ExtDTreeMap.minEntry {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (h : t ≠ ∅) : (a : α) × β a

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

Equations

• t.minEntry h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.minEntry ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.minEntry! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited ((a : α) × β a)] (t : ExtDTreeMap α β 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! = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minEntry!) ⋯ t

@[inline]

def Std.ExtDTreeMap.minEntryD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minEntryD fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.maxEntry? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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? = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxEntry?) ⋯ t

@[inline]

def Std.ExtDTreeMap.maxEntry {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (h : t ≠ ∅) : (a : α) × β a

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

Equations

• t.maxEntry h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.maxEntry ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.maxEntry! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited ((a : α) × β a)] (t : ExtDTreeMap α β 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! = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxEntry!) ⋯ t

@[inline]

def Std.ExtDTreeMap.maxEntryD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxEntryD fallback) ⋯ t

@[inline]

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

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

Equations

• t.minKey? = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minKey?) ⋯ t

@[inline]

def Std.ExtDTreeMap.minKey {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (h : t ≠ ∅) : α

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

Equations

• t.minKey h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.minKey ⋯) ⋯

@[inline]

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

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

Equations

• t.minKey! = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minKey!) ⋯ t

@[inline]

def Std.ExtDTreeMap.minKeyD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (fallback : α) : α

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

Equations

• t.minKeyD fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.minKeyD fallback) ⋯ t

@[inline]

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

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

Equations

• t.maxKey? = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxKey?) ⋯ t

@[inline]

def Std.ExtDTreeMap.maxKey {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (h : t ≠ ∅) : α

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

Equations

• t.maxKey h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.maxKey ⋯) ⋯

@[inline]

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

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

Equations

• t.maxKey! = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxKey!) ⋯ t

@[inline]

def Std.ExtDTreeMap.maxKeyD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (fallback : α) : α

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

Equations

• t.maxKeyD fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.maxKeyD fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.entryAtIdx? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.entryAtIdx? n) ⋯ t

@[inline]

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

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

Equations

• t.entryAtIdx n h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.entryAtIdx n ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.entryAtIdx! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited ((a : α) × β a)] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.entryAtIdx! n) ⋯ t

@[inline]

def Std.ExtDTreeMap.entryAtIdxD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.entryAtIdxD n fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.keyAtIdx? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (n : Nat) : Option α

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

Equations

• t.keyAtIdx? n = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.keyAtIdx? n) ⋯ t

@[inline]

def Std.ExtDTreeMap.keyAtIdx {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (n : Nat) (h : n < t.size) : α

Returns the n-th smallest key.

Equations

• t.keyAtIdx n h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.keyAtIdx n ⋯) ⋯

@[inline]

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

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

Equations

• t.keyAtIdx! n = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.keyAtIdx! n) ⋯ t

@[inline]

def Std.ExtDTreeMap.keyAtIdxD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (n : Nat) (fallback : α) : α

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

Equations

• t.keyAtIdxD n fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.keyAtIdxD n fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryGE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGE? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryGT? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGT? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLE? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLT? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLT? k) ⋯ t

@[inline]

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

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than or equal to the given key.

Equations

• t.getEntryGE k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getEntryGE k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.getEntryGT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : (a : α) × β a

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than the given key.

Equations

• t.getEntryGT k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getEntryGT k ⋯) ⋯

@[inline]

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

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than or equal to the given key.

Equations

• t.getEntryLE k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getEntryLE k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.getEntryLT {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : (a : α) × β a

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than the given key.

Equations

• t.getEntryLT k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getEntryLT k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.getEntryGE! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited (Sigma β)] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGE! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryGT! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited (Sigma β)] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGT! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLE! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited (Sigma β)] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLE! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLT! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited (Sigma β)] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLT! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryGED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (fallback : Sigma β) : (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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGED k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryGTD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (fallback : Sigma β) : (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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryGTD k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (fallback : Sigma β) : (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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLED k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getEntryLTD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (k : α) (fallback : Sigma β) : (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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getEntryLTD k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyGE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGE? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyGT? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGT? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLE? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLE? k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLT? {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLT? k) ⋯ t

@[inline]

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

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

Equations

• t.getKeyGE k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getKeyGE k ⋯) ⋯

@[inline]

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

Given a proof that such a mapping exists, retrieves the smallest key that is greater than the given key.

Equations

• t.getKeyGT k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getKeyGT k ⋯) ⋯

@[inline]

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

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

Equations

• t.getKeyLE k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getKeyLE k ⋯) ⋯

@[inline]

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

Given a proof that such a mapping exists, retrieves the largest key that is less than the given key.

Equations

• t.getKeyLT k h = t.pliftOn (fun (m : Std.DTreeMap α β cmp) (h' : t = Std.ExtDTreeMap.mk m) => m.getKeyLT k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.getKeyGE! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGE! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyGT! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGT! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLE! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLE! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLT! {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Inhabited α] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLT! k) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyGED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGED k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyGTD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyGTD k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLED {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLED k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.getKeyLTD {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β 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.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.getKeyLTD k fallback) ⋯ t

@[inline]

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

@[inline]

def Std.ExtDTreeMap.Const.get? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.get? t a = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.get? m a) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.get {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.get t a h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.get m a ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.Const.get! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.get! t a = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.get! m a) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getD t a fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getD m a fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.minEntry? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.minEntry? t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.minEntry? m) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.minEntry {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (h : t ≠ ∅) : α × β

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

Equations

• Std.ExtDTreeMap.Const.minEntry t h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.minEntry m ⋯) ⋯

@[inline]

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

@[inline]

def Std.ExtDTreeMap.Const.minEntryD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.minEntryD t fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.minEntryD m fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.maxEntry? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.maxEntry? t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.maxEntry? m) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.maxEntry {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (h : t ≠ ∅) : α × β

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

Equations

• Std.ExtDTreeMap.Const.maxEntry t h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.maxEntry m ⋯) ⋯

@[inline]

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

@[inline]

def Std.ExtDTreeMap.Const.maxEntryD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.maxEntryD t fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.maxEntryD m fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.entryAtIdx? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.entryAtIdx? t n = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.entryAtIdx? m n) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.entryAtIdx {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (n : Nat) (h : n < t.size) : α × β

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

Equations

• Std.ExtDTreeMap.Const.entryAtIdx t n h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.entryAtIdx m n ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.Const.entryAtIdx! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] [Inhabited (α × β)] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.entryAtIdx! t n = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.entryAtIdx! m n) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.entryAtIdxD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.entryAtIdxD t n fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.entryAtIdxD m n fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryGE? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryGE? t k = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryGE? m k) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryGT? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryGT? t k = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryGT? m k) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryLE? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryLE? t k = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryLE? m k) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryLT? {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryLT? t k = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryLT? m k) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryGE {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isGE = true) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than or equal to the given key.

Equations

• Std.ExtDTreeMap.Const.getEntryGE t k h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.getEntryGE m k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.Const.getEntryGT {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.gt) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is greater than the given key.

Equations

• Std.ExtDTreeMap.Const.getEntryGT t k h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.getEntryGT m k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.Const.getEntryLE {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ (cmp a k).isLE = true) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than or equal to the given key.

Equations

• Std.ExtDTreeMap.Const.getEntryLE t k h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.getEntryLE m k ⋯) ⋯

@[inline]

def Std.ExtDTreeMap.Const.getEntryLT {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (k : α) (h : ∃ (a : α), a ∈ t ∧ cmp a k = Ordering.lt) : α × β

Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is less than the given key.

Equations

• Std.ExtDTreeMap.Const.getEntryLT t k h = t.pliftOn (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) (h' : t = Std.ExtDTreeMap.mk m) => Std.DTreeMap.Const.getEntryLT m k ⋯) ⋯

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

def Std.ExtDTreeMap.Const.getEntryLT! {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] [Inhabited (α × β)] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryLT! t k = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryLT! m k) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryGED {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryGED t k fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryGED m k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryGTD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryGTD t k fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryGTD m k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryLED {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryLED t k fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryLED m k fallback) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.getEntryLTD {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (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.ExtDTreeMap.Const.getEntryLTD t k fallback = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.getEntryLTD m k fallback) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.filter f t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.filter f m)) ⋯ t

@[inline]

def Std.ExtDTreeMap.filterMap {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} (f : (a : α) → β a → Option (γ a)) (t : ExtDTreeMap α β cmp) : ExtDTreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings, keeping only those mappings where the function returns some value.

Equations

• Std.ExtDTreeMap.filterMap f t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.filterMap f m)) ⋯ t

@[inline]

def Std.ExtDTreeMap.map {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} (f : (a : α) → β a → γ a) (t : ExtDTreeMap α β cmp) : ExtDTreeMap α γ cmp

Updates the values of the map by applying the given function to all mappings.

Equations

• Std.ExtDTreeMap.map f t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.map f m)) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.foldlM f init t = Std.ExtDTreeMap.lift (fun (m_1 : Std.DTreeMap α β cmp) => Std.DTreeMap.foldlM f init m_1) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.foldl f init t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.DTreeMap.foldl f init m) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.foldrM f init t = Std.ExtDTreeMap.lift (fun (m_1 : Std.DTreeMap α β cmp) => Std.DTreeMap.foldrM f init m_1) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.foldr f init t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.DTreeMap.foldr f init m) ⋯ t

@[inline]

def Std.ExtDTreeMap.partition {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (f : (a : α) → β a → Bool) (t : ExtDTreeMap α β cmp) : ExtDTreeMap α β cmp × ExtDTreeMap α β 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.

@[inline]

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

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

Equations

• Std.ExtDTreeMap.forM f t = Std.ExtDTreeMap.lift (fun (m_1 : Std.DTreeMap α β cmp) => Std.DTreeMap.forM f m_1) ⋯ t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.forIn f init t = Std.ExtDTreeMap.lift (fun (m_1 : Std.DTreeMap α β cmp) => Std.DTreeMap.forIn f init m_1) ⋯ t

instance Std.ExtDTreeMap.instForMSigmaOfTransCmpOfLawfulMonad {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForM m (ExtDTreeMap α β cmp) ((a : α) × β a)

Equations

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

instance Std.ExtDTreeMap.instForInSigmaOfTransCmpOfLawfulMonad {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [TransCmp cmp] [inst : Monad m] [LawfulMonad m] : ForIn m (ExtDTreeMap α β 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 ExtDTreeMap.

@[inline]

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

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

Equations

• Std.ExtDTreeMap.Const.forMUncurried f t = Std.ExtDTreeMap.forM (fun (a : α) (b : β) => f (a, b)) t

@[inline]

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

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

Equations

• Std.ExtDTreeMap.Const.forInUncurried f init t = Std.ExtDTreeMap.forIn (fun (a : α) (b : β) (acc : δ) => f (a, b) acc) init t

@[inline]

def Std.ExtDTreeMap.any {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool

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

Equations

• t.any p = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.any p) ⋯ t

@[inline]

def Std.ExtDTreeMap.all {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool

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

Equations

• t.all p = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.all p) ⋯ t

@[inline]

def Std.ExtDTreeMap.keys {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) : List α

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

Equations

• t.keys = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.keys) ⋯ t

@[inline]

def Std.ExtDTreeMap.keysArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) : Array α

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

Equations

• t.keysArray = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.keysArray) ⋯ t

@[inline]

def Std.ExtDTreeMap.values {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {β : Type v} (t : ExtDTreeMap α (fun (x : α) => β) cmp) : List β

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

Equations

• t.values = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => m.values) ⋯ t

@[inline]

def Std.ExtDTreeMap.valuesArray {α : Type u} {cmp : α → α → Ordering} [TransCmp cmp] {β : Type v} (t : ExtDTreeMap α (fun (x : α) => β) cmp) : Array β

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

Equations

• t.valuesArray = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => m.valuesArray) ⋯ t

@[inline]

def Std.ExtDTreeMap.toList {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) : List ((a : α) × β a)

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

Equations

• t.toList = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.toList) ⋯ t

@[inline]

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

Transforms a list of mappings into a tree map.

Equations

• Std.ExtDTreeMap.ofList l cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.ofList l cmp)

@[inline]

def Std.ExtDTreeMap.toArray {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] (t : ExtDTreeMap α β cmp) : Array ((a : α) × β a)

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

Equations

• t.toArray = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => m.toArray) ⋯ t

@[inline]

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

Transforms an array of mappings into a tree map.

Equations

• Std.ExtDTreeMap.ofArray a cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.ofArray a cmp)

@[inline]

def Std.ExtDTreeMap.modify {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (f : β a → β a) : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (m.modify a f)) ⋯ t

@[inline]

def Std.ExtDTreeMap.alter {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (t : ExtDTreeMap α β cmp) (a : α) (f : Option (β a) → Option (β a)) : ExtDTreeMap α β 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 = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (m.alter a f)) ⋯ t

@[inline]

def Std.ExtDTreeMap.mergeWith {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (mergeFn : (a : α) → β a → β a → β a) (t₁ t₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β 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.ExtDTreeMap.mergeWith mergeFn t₁ t₂ = t₁.liftOn₂ t₂ (fun (m₁ m₂ : Std.DTreeMap α β cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.mergeWith mergeFn m₁ m₂)) ⋯

@[inline]

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

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

Equations

• Std.ExtDTreeMap.Const.toList t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.toList m) ⋯ t

@[inline]

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

Transforms a list of mappings into a tree map.

Equations

• Std.ExtDTreeMap.Const.ofList l cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.Const.ofList l cmp)

@[inline]

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

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

Equations

• Std.ExtDTreeMap.Const.toArray t = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.DTreeMap.Const.toArray m) ⋯ t

@[inline]

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

Transforms a list of mappings into a tree map.

Equations

• Std.ExtDTreeMap.Const.ofArray a cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.Const.ofArray a cmp)

@[inline]

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

Transforms a list of keys into a tree map.

Equations

• Std.ExtDTreeMap.Const.unitOfList l cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.Const.unitOfList l cmp)

@[inline]

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

Transforms an array of keys into a tree map.

Equations

• Std.ExtDTreeMap.Const.unitOfArray a cmp = Std.ExtDTreeMap.mk (Std.DTreeMap.Const.unitOfArray a cmp)

@[inline]

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

Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.

Equations

• Std.ExtDTreeMap.Const.modify t a f = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.Const.modify m a f)) ⋯ t

@[inline]

def Std.ExtDTreeMap.Const.alter {α : Type u} {cmp : α → α → Ordering} {β : Type v} [TransCmp cmp] (t : ExtDTreeMap α (fun (x : α) => β) cmp) (a : α) (f : Option β → Option β) : ExtDTreeMap α (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.ExtDTreeMap.Const.alter t a f = Std.ExtDTreeMap.lift (fun (m : Std.DTreeMap α (fun (x : α) => β) cmp) => Std.ExtDTreeMap.mk (Std.DTreeMap.Const.alter m a f)) ⋯ t

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

Equations

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

@[inline]

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

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

@[inline]

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

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

instance Std.ExtDTreeMap.instReprOfTransCmp {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [TransCmp cmp] [Repr α] [(a : α) → Repr (β a)] : Repr (ExtDTreeMap α β cmp)

Equations

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