Low-level implementation of the size-bounded tree

This file contains the basic definition implementing the functionality of the size-bounded trees.

structure Std.DTreeMap.Internal.Impl.Equiv {α : Type u} {β : α → Type v} (t t' : Impl α β) : Prop

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

• impl : t.toListModel.Perm t'.toListModel

  Implementation detail of the tree map

def Std.DTreeMap.Internal.Impl.«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.

def Std.DTreeMap.Internal.Impl.contains {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) : Bool

Returns true if the given key is contained in the map.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.contains k Std.DTreeMap.Internal.Impl.leaf = false

instance Std.DTreeMap.Internal.Impl.instMembershipOfOrd {α : Type u} {β : α → Type v} [Ord α] : Membership α (Impl α β)

Equations

• Std.DTreeMap.Internal.Impl.instMembershipOfOrd = { mem := fun (t : Std.DTreeMap.Internal.Impl α β) (a : α) => Std.DTreeMap.Internal.Impl.contains a t = true }

theorem Std.DTreeMap.Internal.Impl.mem_iff_contains {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {k : α} : k ∈ t ↔ contains k t = true

theorem Std.DTreeMap.Internal.Impl.contains_iff_mem {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {k : α} : contains k t = true ↔ k ∈ t

instance Std.DTreeMap.Internal.Impl.instDecidableMem {α : Type u} {β : α → Type v} [Ord α] {m : Impl α β} {a : α} : Decidable (a ∈ m)

Equations

• Std.DTreeMap.Internal.Impl.instDecidableMem = inferInstanceAs (Decidable (Std.DTreeMap.Internal.Impl.contains a m = true))

theorem Std.DTreeMap.Internal.Impl.Ordered.mem_inner_iff_mem_right {α : Type u} {β : α → Type v} [Ord α] (sz : Nat) (a : α) (v : β a) (l r : Impl α β) (k : α) (h : compare k a = Ordering.gt) : k ∈ inner sz a v l r ↔ k ∈ r

theorem Std.DTreeMap.Internal.Impl.Ordered.mem_inner_iff_mem_left {α : Type u} {β : α → Type v} [Ord α] (sz : Nat) (a : α) (v : β a) (l r : Impl α β) (k : α) (h : compare k a = Ordering.lt) : k ∈ inner sz a v l r ↔ k ∈ l

@[inline]

def Std.DTreeMap.Internal.Impl.isEmpty {α : Type u} {β : α → Type v} (t : Impl α β) : Bool

Returns true if the tree is empty.

Equations

• Std.DTreeMap.Internal.Impl.leaf.isEmpty = true
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).isEmpty = false

def Std.DTreeMap.Internal.Impl.get? {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) : Option (β k)

Returns the value for the key k, or none if such a key does not exist.

Equations

• Std.DTreeMap.Internal.Impl.leaf.get? k = none
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).get? k = match h : compare k k' with | Ordering.lt => l.get? k | Ordering.gt => r.get? k | Ordering.eq => some (cast ⋯ v)

def Std.DTreeMap.Internal.Impl.get {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (hlk : k ∈ t) : β k

Returns the value for the key k.

Equations

• (Std.DTreeMap.Internal.Impl.inner size k' v' l r).get k hlk_2 = match h : compare k k' with | Ordering.lt => l.get k ⋯ | Ordering.gt => r.get k ⋯ | Ordering.eq => cast ⋯ v'

def Std.DTreeMap.Internal.Impl.get! {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) [Inhabited (β k)] : β k

Returns the value for the key k, or panics if such a key does not exist.

Equations

• Std.DTreeMap.Internal.Impl.leaf.get! k = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.get!" 99 13 "Key is not present in map"
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).get! k = match h : compare k k' with | Ordering.lt => l.get! k | Ordering.gt => r.get! k | Ordering.eq => cast ⋯ v

def Std.DTreeMap.Internal.Impl.getD {α : Type u} {β : α → Type v} [Ord α] [LawfulEqOrd α] (t : Impl α β) (k : α) (fallback : β k) : β k

Returns the value for the key k, or fallback if such a key does not exist.

Equations

• Std.DTreeMap.Internal.Impl.leaf.getD k fallback = fallback
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).getD k fallback = match h : compare k k' with | Ordering.lt => l.getD k fallback | Ordering.gt => r.getD k fallback | Ordering.eq => cast ⋯ v

def Std.DTreeMap.Internal.Impl.getKey? {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (k : α) : Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.getKey? k = none
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey? k = match compare k k' with | Ordering.lt => l.getKey? k | Ordering.gt => r.getKey? k | Ordering.eq => some k'

def Std.DTreeMap.Internal.Impl.getKey {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (k : α) (hlk : contains k t = true) : α

Implementation detail of the tree map

Equations

• (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey k hlk_2 = match h : compare k k' with | Ordering.lt => l.getKey k ⋯ | Ordering.gt => r.getKey k ⋯ | Ordering.eq => k'

def Std.DTreeMap.Internal.Impl.getKey! {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (k : α) [Inhabited α] : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.getKey! k = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getKey!" 138 13 "Key is not present in map"
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKey! k = match compare k k' with | Ordering.lt => l.getKey! k | Ordering.gt => r.getKey! k | Ordering.eq => k'

def Std.DTreeMap.Internal.Impl.getKeyD {α : Type u} {β : α → Type v} [Ord α] (t : Impl α β) (k fallback : α) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.getKeyD k fallback = fallback
• (Std.DTreeMap.Internal.Impl.inner size k' v l r).getKeyD k fallback = match compare k k' with | Ordering.lt => l.getKeyD k fallback | Ordering.gt => r.getKeyD k fallback | Ordering.eq => k'

def Std.DTreeMap.Internal.Impl.Const.get? {α : Type u} {δ : Type w} [Ord α] (t : Impl α fun (x : α) => δ) (k : α) : Option δ

Returns the value for the key k, or none if such a key does not exist.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.get? Std.DTreeMap.Internal.Impl.leaf k = none

def Std.DTreeMap.Internal.Impl.Const.get {α : Type u} {δ : Type w} [Ord α] (t : Impl α fun (x : α) => δ) (k : α) (hlk : contains k t = true) : δ

Returns the value for the key k.

Equations

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

def Std.DTreeMap.Internal.Impl.Const.get! {α : Type u} {δ : Type w} [Ord α] (t : Impl α fun (x : α) => δ) (k : α) [Inhabited δ] : δ

Returns the value for the key k, or panics if such a key does not exist.

Equations

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

def Std.DTreeMap.Internal.Impl.Const.getD {α : Type u} {δ : Type w} [Ord α] (t : Impl α fun (x : α) => δ) (k : α) (fallback : δ) : δ

Returns the value for the key k, or fallback if such a key does not exist.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getD Std.DTreeMap.Internal.Impl.leaf k fallback = fallback

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.foldlM {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [Monad m] (f : δ → (a : α) → β a → m δ) (init : δ) : Impl α β → m δ

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

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.foldlM f init Std.DTreeMap.Internal.Impl.leaf = pure init

@[specialize #[]]

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

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

Equations

• Std.DTreeMap.Internal.Impl.foldl f init t = (Std.DTreeMap.Internal.Impl.foldlM (fun (x1 : δ) (x2 : α) (x3 : β x2) => pure (f x1 x2 x3)) init t).run

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.foldrM {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [Monad m] (f : (a : α) → β a → δ → m δ) (init : δ) : Impl α β → m δ

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

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.foldrM f init Std.DTreeMap.Internal.Impl.leaf = pure init

@[inline]

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

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

Equations

• Std.DTreeMap.Internal.Impl.foldr f init t = (Std.DTreeMap.Internal.Impl.foldrM (fun (x1 : α) (x2 : β x1) (x3 : δ) => pure (f x1 x2 x3)) init t).run

@[inline]

def Std.DTreeMap.Internal.Impl.forM {α : Type u} {β : α → Type v} {m : Type u_1 → Type u_2} [Monad m] (f : (a : α) → β a → m PUnit) (t : Impl α β) : m PUnit

Applies the given function to the mappings in the tree in ascending order.

Equations

• Std.DTreeMap.Internal.Impl.forM f t = Std.DTreeMap.Internal.Impl.foldlM (fun (x : PUnit) (k : α) (v : β k) => f k v) PUnit.unit t

@[specialize #[]]

def Std.DTreeMap.Internal.Impl.forInStep {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) : Impl α β → m (ForInStep δ)

Implementation detail.

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.forInStep f init Std.DTreeMap.Internal.Impl.leaf = pure (ForInStep.yield init)

@[inline]

def Std.DTreeMap.Internal.Impl.forIn {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (t : Impl α β) : m δ

Support for the for construct in do blocks.

Equations

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

@[inline]

def Std.DTreeMap.Internal.Impl.keys {α : Type u} {β : α → Type v} (t : Impl α β) : List α

Returns a List of the keys in order.

Equations

• t.keys = Std.DTreeMap.Internal.Impl.foldr (fun (k : α) (x : β k) (l : List α) => k :: l) [] t

@[inline]

def Std.DTreeMap.Internal.Impl.keysArray {α : Type u} {β : α → Type v} (t : Impl α β) : Array α

Returns an Array of the keys in order.

Equations

• t.keysArray = Std.DTreeMap.Internal.Impl.foldl (fun (l : Array α) (k : α) (x : β k) => l.push k) (Array.emptyWithCapacity t.size) t

@[inline]

def Std.DTreeMap.Internal.Impl.values {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) : List β

Returns a List of the values in order.

Equations

• t.values = Std.DTreeMap.Internal.Impl.foldr (fun (x : α) (v : β) (l : List β) => v :: l) [] t

@[inline]

def Std.DTreeMap.Internal.Impl.valuesArray {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) : Array β

Returns an Array of the values in order.

Equations

• t.valuesArray = Std.DTreeMap.Internal.Impl.foldl (fun (l : Array β) (x : α) (v : β) => l.push v) (Array.emptyWithCapacity t.size) t

@[inline]

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

Returns a List of the key/value pairs in order.

Equations

• t.toList = Std.DTreeMap.Internal.Impl.foldr (fun (k : α) (v : β k) (l : List ((a : α) × β a)) => ⟨k, v⟩ :: l) [] t

@[inline]

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

Returns an Array of the key/value pairs in order.

Equations

• t.toArray = Std.DTreeMap.Internal.Impl.foldl (fun (l : Array ((a : α) × β a)) (k : α) (v : β k) => l.push ⟨k, v⟩) (Array.emptyWithCapacity t.size) t

@[inline]

def Std.DTreeMap.Internal.Impl.Const.toList {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) : List (α × β)

Returns a List of the key/value pairs in order.

Equations

• Std.DTreeMap.Internal.Impl.Const.toList t = Std.DTreeMap.Internal.Impl.foldr (fun (k : α) (v : β) (l : List (α × β)) => (k, v) :: l) [] t

@[inline]

def Std.DTreeMap.Internal.Impl.Const.toArray {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) : Array (α × β)

Returns a List of the key/value pairs in order.

Equations

• Std.DTreeMap.Internal.Impl.Const.toArray t = Std.DTreeMap.Internal.Impl.foldl (fun (l : Array (α × β)) (k : α) (v : β) => l.push (k, v)) (Array.emptyWithCapacity t.size) t

@[irreducible]

def Std.DTreeMap.Internal.Impl.minEntry? {α : Type u} {β : α → Type v} : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minEntry? = none
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry? = some ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry? = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry?

@[irreducible]

def Std.DTreeMap.Internal.Impl.minEntry {α : Type u} {β : α → Type v} (t : Impl α β) (h : t.isEmpty = false) : (a : α) × β a

Implementation detail of the tree map

Equations

• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry x_2 = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry ⋯

@[irreducible]

def Std.DTreeMap.Internal.Impl.minEntry! {α : Type u} {β : α → Type v} [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minEntry! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minEntry!" 302 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntry! = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry! = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry!

@[irreducible]

def Std.DTreeMap.Internal.Impl.minEntryD {α : Type u} {β : α → Type v} : Impl α β → (a : α) × β a → (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minEntryD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minEntryD x✝ = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntryD x✝ = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntryD x✝

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxEntry? {α : Type u} {β : α → Type v} : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxEntry? = none
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry? = some ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntry? = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry?

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxEntry {α : Type u} {β : α → Type v} (t : Impl α β) (h : t.isEmpty = false) : (a : α) × β a

Implementation detail of the tree map

Equations

• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry x_2 = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntry h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry ⋯

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxEntry! {α : Type u} {β : α → Type v} [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxEntry! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxEntry!" 325 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntry! = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntry! = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry!

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxEntryD {α : Type u} {β : α → Type v} : Impl α β → (a : α) × β a → (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxEntryD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxEntryD x✝ = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntryD x✝ = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntryD x✝

@[irreducible]

def Std.DTreeMap.Internal.Impl.minKey? {α : Type u} {β : α → Type v} : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minKey? = none
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minKey? = some k
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minKey? = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey?

@[irreducible]

def Std.DTreeMap.Internal.Impl.minKey {α : Type u} {β : α → Type v} (t : Impl α β) (h : t.isEmpty = false) : α

Implementation detail of the tree map

Equations

• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minKey x_2 = k
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minKey h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey ⋯

@[irreducible]

def Std.DTreeMap.Internal.Impl.minKey! {α : Type u} {β : α → Type v} [Inhabited α] : Impl α β → α

The smallest key of t. Returns the given fallback value if the map is empty.

Equations

• Std.DTreeMap.Internal.Impl.leaf.minKey! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minKey!" 348 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minKey! = k
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minKey! = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey!

@[irreducible]

def Std.DTreeMap.Internal.Impl.minKeyD {α : Type u} {β : α → Type v} : Impl α β → α → α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minKeyD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minKeyD x✝ = k
• (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minKeyD x✝ = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKeyD x✝

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxKey? {α : Type u} {β : α → Type v} : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxKey? = none
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKey? = some k
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKey? = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey?

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxKey {α : Type u} {β : α → Type v} (t : Impl α β) (h : t.isEmpty = false) : α

Implementation detail of the tree map

Equations

• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKey x_2 = k
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKey h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey ⋯

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxKey! {α : Type u} {β : α → Type v} [Inhabited α] : Impl α β → α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxKey! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxKey!" 371 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKey! = k
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKey! = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey!

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxKeyD {α : Type u} {β : α → Type v} : Impl α β → α → α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxKeyD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxKeyD x✝ = k
• (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxKeyD x✝ = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKeyD x✝

def Std.DTreeMap.Internal.Impl.entryAtIdx {α : Type u} {β : α → Type v} (t : Impl α β) (hl : t.Balanced) (n : Nat) (h : n < t.size) : (a : α) × β a

Implementation detail of the tree map

Equations

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

def Std.DTreeMap.Internal.Impl.entryAtIdx? {α : Type u} {β : α → Type v} : Impl α β → Nat → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.entryAtIdx? x✝ = none

def Std.DTreeMap.Internal.Impl.entryAtIdx! {α : Type u} {β : α → Type v} [Inhabited ((a : α) × β a)] : Impl α β → Nat → (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.entryAtIdx! x✝ = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.entryAtIdx!" 402 16 "Out-of-bounds access"

def Std.DTreeMap.Internal.Impl.entryAtIdxD {α : Type u} {β : α → Type v} : Impl α β → Nat → (a : α) × β a → (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.entryAtIdxD x✝¹ x✝ = x✝

def Std.DTreeMap.Internal.Impl.keyAtIdx {α : Type u} {β : α → Type v} (t : Impl α β) (hl : t.Balanced) (n : Nat) (h : n < t.size) : α

Implementation detail of the tree map

Equations

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

def Std.DTreeMap.Internal.Impl.keyAtIdx? {α : Type u} {β : α → Type v} : Impl α β → Nat → Option α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.keyAtIdx? x✝ = none

def Std.DTreeMap.Internal.Impl.keyAtIdx! {α : Type u} {β : α → Type v} [Inhabited α] : Impl α β → Nat → α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.keyAtIdx! x✝ = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.keyAtIdx!" 438 16 "Out-of-bounds access"
• (Std.DTreeMap.Internal.Impl.inner size k v l r).keyAtIdx! x✝ = match compare x✝ l.size with | Ordering.lt => l.keyAtIdx! x✝ | Ordering.eq => k | Ordering.gt => r.keyAtIdx! (x✝ - l.size - 1)

def Std.DTreeMap.Internal.Impl.keyAtIdxD {α : Type u} {β : α → Type v} : Impl α β → Nat → α → α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.leaf.keyAtIdxD x✝¹ x✝ = x✝

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryGE? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGE? k = Std.DTreeMap.Internal.Impl.getEntryGE?.go k none

def Std.DTreeMap.Internal.Impl.getEntryGE?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option ((a : α) × β a)) : Impl α β → Option ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryGT? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGT? k = Std.DTreeMap.Internal.Impl.getEntryGT?.go k none

def Std.DTreeMap.Internal.Impl.getEntryGT?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option ((a : α) × β a)) : Impl α β → Option ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryLE? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLE? k = Std.DTreeMap.Internal.Impl.getEntryLE?.go k none

def Std.DTreeMap.Internal.Impl.getEntryLE?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option ((a : α) × β a)) : Impl α β → Option ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryLT? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option ((a : α) × β a)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLT? k = Std.DTreeMap.Internal.Impl.getEntryLT?.go k none

def Std.DTreeMap.Internal.Impl.getEntryLT?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option ((a : α) × β a)) : Impl α β → Option ((a : α) × β a)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGE! k t = (Std.DTreeMap.Internal.Impl.getEntryGE? k t).get!

@[inline]

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGT! k t = (Std.DTreeMap.Internal.Impl.getEntryGT? k t).get!

@[inline]

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLE! k t = (Std.DTreeMap.Internal.Impl.getEntryLE? k t).get!

@[inline]

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLT! k t = (Std.DTreeMap.Internal.Impl.getEntryLT? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryGED {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : (a : α) × β a) : (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryGTD {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : (a : α) × β a) : (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryGTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGT? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryLED {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : (a : α) × β a) : (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLED k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getEntryLTD {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : (a : α) × β a) : (a : α) × β a

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getEntryLTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryLT? k t).getD fallback

def Std.DTreeMap.Internal.Impl.getEntryGE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true) : (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getEntryGT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt) : (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getEntryLE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true) : (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getEntryLT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt) : (a : α) × β a

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getEntryLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGE? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGE? k = Std.DTreeMap.Internal.Impl.getKeyGE?.go k none

def Std.DTreeMap.Internal.Impl.getKeyGE?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option α) : Impl α β → Option α

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGT? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGT? k = Std.DTreeMap.Internal.Impl.getKeyGT?.go k none

def Std.DTreeMap.Internal.Impl.getKeyGT?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option α) : Impl α β → Option α

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLE? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLE? k = Std.DTreeMap.Internal.Impl.getKeyLE?.go k none

def Std.DTreeMap.Internal.Impl.getKeyLE?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option α) : Impl α β → Option α

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLT? {α : Type u} {β : α → Type v} [Ord α] (k : α) : Impl α β → Option α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLT? k = Std.DTreeMap.Internal.Impl.getKeyLT?.go k none

def Std.DTreeMap.Internal.Impl.getKeyLT?.go {α : Type u} {β : α → Type v} [Ord α] (k : α) (best : Option α) : Impl α β → Option α

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGE! {α : Type u} {β : α → Type v} [Ord α] [Inhabited α] (k : α) (t : Impl α β) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGE! k t = (Std.DTreeMap.Internal.Impl.getKeyGE? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGT! {α : Type u} {β : α → Type v} [Ord α] [Inhabited α] (k : α) (t : Impl α β) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGT! k t = (Std.DTreeMap.Internal.Impl.getKeyGT? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLE! {α : Type u} {β : α → Type v} [Ord α] [Inhabited α] (k : α) (t : Impl α β) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLE! k t = (Std.DTreeMap.Internal.Impl.getKeyLE? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLT! {α : Type u} {β : α → Type v} [Ord α] [Inhabited α] (k : α) (t : Impl α β) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLT! k t = (Std.DTreeMap.Internal.Impl.getKeyLT? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGED {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : α) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyGTD {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : α) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyGTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGT? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLED {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : α) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.getKeyLTD {α : Type u} {β : α → Type v} [Ord α] (k : α) (t : Impl α β) (fallback : α) : α

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.getKeyLTD k t fallback = (Std.DTreeMap.Internal.Impl.getKeyLT? k t).getD fallback

def Std.DTreeMap.Internal.Impl.getKeyGE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true) : α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getKeyGT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt) : α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getKeyLE {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true) : α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.getKeyLT {α : Type u} {β : α → Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt) : α

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.getKeyLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

@[irreducible]

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

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.minEntry? Std.DTreeMap.Internal.Impl.leaf = none
• Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) = some (k, v)

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.minEntry {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) (h : t.isEmpty = false) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.minEntry (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x_2 = (k, v)

@[irreducible]

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

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.minEntry! (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) = (k, v)

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.minEntryD {α : Type u} {β : Type v} : (Impl α fun (x : α) => β) → α × β → α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.minEntryD Std.DTreeMap.Internal.Impl.leaf x✝ = x✝
• Std.DTreeMap.Internal.Impl.Const.minEntryD (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x✝ = (k, v)

@[irreducible]

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

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.maxEntry? Std.DTreeMap.Internal.Impl.leaf = none
• Std.DTreeMap.Internal.Impl.Const.maxEntry? (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) = some (k, v)

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.maxEntry {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) (h : t.isEmpty = false) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.maxEntry (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x_2 = (k, v)

@[irreducible]

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

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.maxEntry! (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) = (k, v)

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.maxEntryD {α : Type u} {β : Type v} : (Impl α fun (x : α) => β) → α × β → α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.maxEntryD Std.DTreeMap.Internal.Impl.leaf x✝ = x✝
• Std.DTreeMap.Internal.Impl.Const.maxEntryD (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x✝ = (k, v)

@[inline]

def Std.DTreeMap.Internal.Impl.Const.entryAtIdx {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) (hl : t.Balanced) (n : Nat) (h : n < t.size) : α × β

Implementation detail of the tree map

Equations

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

def Std.DTreeMap.Internal.Impl.Const.entryAtIdx? {α : Type u} {β : Type v} : (Impl α fun (x : α) => β) → Nat → Option (α × β)

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.entryAtIdx? Std.DTreeMap.Internal.Impl.leaf x✝ = none

def Std.DTreeMap.Internal.Impl.Const.entryAtIdx! {α : Type u} {β : Type v} [Inhabited (α × β)] : (Impl α fun (x : α) => β) → Nat → α × β

Implementation detail of the tree map

Equations

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

def Std.DTreeMap.Internal.Impl.Const.entryAtIdxD {α : Type u} {β : Type v} : (Impl α fun (x : α) => β) → Nat → α × β → α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.entryAtIdxD Std.DTreeMap.Internal.Impl.leaf x✝¹ x✝ = x✝

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGE? {α : Type u} {β : Type v} [Ord α] (k : α) : (Impl α fun (x : α) => β) → Option (α × β)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGE? k = Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k none

def Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) : (Impl α fun (x : α) => β) → Option (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGT? {α : Type u} {β : Type v} [Ord α] (k : α) : (Impl α fun (x : α) => β) → Option (α × β)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGT? k = Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k none

def Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) : (Impl α fun (x : α) => β) → Option (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLE? {α : Type u} {β : Type v} [Ord α] (k : α) : (Impl α fun (x : α) => β) → Option (α × β)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLE? k = Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k none

def Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) : (Impl α fun (x : α) => β) → Option (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLT? {α : Type u} {β : Type v} [Ord α] (k : α) : (Impl α fun (x : α) => β) → Option (α × β)

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLT? k = Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k none

def Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) : (Impl α fun (x : α) => β) → Option (α × β)

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go k best Std.DTreeMap.Internal.Impl.leaf = best

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGE! {α : Type u} {β : Type v} [Ord α] [Inhabited (α × β)] (k : α) (t : Impl α fun (x : α) => β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGE! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGT! {α : Type u} {β : Type v} [Ord α] [Inhabited (α × β)] (k : α) (t : Impl α fun (x : α) => β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGT! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLE! {α : Type u} {β : Type v} [Ord α] [Inhabited (α × β)] (k : α) (t : Impl α fun (x : α) => β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLE! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLT! {α : Type u} {β : Type v} [Ord α] [Inhabited (α × β)] (k : α) (t : Impl α fun (x : α) => β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLT! k t = (Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t).get!

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGED {α : Type u} {β : Type v} [Ord α] (k : α) (t : Impl α fun (x : α) => β) (fallback : α × β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGED k t fallback = (Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryGTD {α : Type u} {β : Type v} [Ord α] (k : α) (t : Impl α fun (x : α) => β) (fallback : α × β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryGTD k t fallback = (Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLED {α : Type u} {β : Type v} [Ord α] (k : α) (t : Impl α fun (x : α) => β) (fallback : α × β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLED k t fallback = (Std.DTreeMap.Internal.Impl.Const.getEntryLE? k t).getD fallback

@[inline]

def Std.DTreeMap.Internal.Impl.Const.getEntryLTD {α : Type u} {β : Type v} [Ord α] (k : α) (t : Impl α fun (x : α) => β) (fallback : α × β) : α × β

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t fallback = (Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t).getD fallback

def Std.DTreeMap.Internal.Impl.Const.getEntryGE {α : Type u} {β : Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α fun (x : α) => β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isGE = true) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryGE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.Const.getEntryGT {α : Type u} {β : Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α fun (x : α) => β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.gt) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryGT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.Const.getEntryLE {α : Type u} {β : Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α fun (x : α) => β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ (compare a k).isLE = true) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryLE k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim

def Std.DTreeMap.Internal.Impl.Const.getEntryLT {α : Type u} {β : Type v} [Ord α] [TransOrd α] (k : α) (t : Impl α fun (x : α) => β) (ho : t.Ordered) (he : ∃ (a : α), a ∈ t ∧ compare a k = Ordering.lt) : α × β

Implementation detail of the tree map

Equations

• One or more equations did not get rendered due to their size.
• Std.DTreeMap.Internal.Impl.Const.getEntryLT k Std.DTreeMap.Internal.Impl.leaf x_3 he = ⋯.elim