Low-level implementation of the size-bounded tree

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

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 }

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 : contains k t = true) : β 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!" 86 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!" 125 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 f 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 f 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) #[] 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) #[] 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⟩) #[] 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)) #[] t

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.min? = none
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).min? = some ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).min? = l.min?

@[irreducible]

def Std.DTreeMap.Internal.Impl.min {α : Type u} {β : α → Type v} [Ord α] (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).min 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).min h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).min ⋯

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.min! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.min!" 289 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).min! = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).min! = l.min!

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.minD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).minD x✝ = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).minD x✝ = l.minD x✝

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.max? = none
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).max? = some ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).max? = r.max?

@[irreducible]

def Std.DTreeMap.Internal.Impl.max {α : Type u} {β : α → Type v} [Ord α] (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).max 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).max h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).max ⋯

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.max! = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.max!" 312 13 "Map is empty"
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).max! = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).max! = r.max!

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.leaf.maxD x✝ = x✝
• (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).maxD x✝ = ⟨k, v⟩
• (Std.DTreeMap.Internal.Impl.inner size k v l r).maxD x✝ = r.maxD x✝

def Std.DTreeMap.Internal.Impl.minKey? {α : Type u} {β : α → Type v} [Ord α] : 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 l r).minKey? = l.minKey?

@[irreducible]

def Std.DTreeMap.Internal.Impl.minKey {α : Type u} {β : α → Type v} [Ord α] (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 ⋯

def Std.DTreeMap.Internal.Impl.minKey! {α : Type u} {β : α → Type v} [Ord α] [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!" 335 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 l r).minKey! = l.minKey!

def Std.DTreeMap.Internal.Impl.minKeyD {α : Type u} {β : α → Type v} [Ord α] : 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 l r).minKeyD x✝ = l.minKeyD x✝

def Std.DTreeMap.Internal.Impl.maxKey? {α : Type u} {β : α → Type v} [Ord α] : 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 r).maxKey? = r.maxKey?

@[irreducible]

def Std.DTreeMap.Internal.Impl.maxKey {α : Type u} {β : α → Type v} [Ord α] (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).maxKey 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).maxKey h = (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).maxKey ⋯

def Std.DTreeMap.Internal.Impl.maxKey! {α : Type u} {β : α → Type v} [Ord α] [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!" 358 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 r).maxKey! = r.maxKey!

def Std.DTreeMap.Internal.Impl.maxKeyD {α : Type u} {β : α → Type v} [Ord α] : 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 r).maxKeyD x✝ = r.maxKeyD x✝

def Std.DTreeMap.Internal.Impl.entryAtIdx {α : Type u} {β : α → Type v} [Ord α] (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} [Ord α] : 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} [Ord α] [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!" 389 16 "Out-of-bounds access"

def Std.DTreeMap.Internal.Impl.entryAtIdxD {α : Type u} {β : α → Type v} [Ord α] : 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.keyAtIndex {α : Type u} {β : α → Type v} [Ord α] (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.keyAtIndex? {α : Type u} {β : α → Type v} [Ord α] : 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.keyAtIndex? x✝ = none

def Std.DTreeMap.Internal.Impl.keyAtIndex! {α : Type u} {β : α → Type v} [Ord α] [Inhabited α] : 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.keyAtIndex! x✝ = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.keyAtIndex!" 425 16 "Out-of-bounds access"

def Std.DTreeMap.Internal.Impl.keyAtIndexD {α : Type u} {β : α → Type v} [Ord α] : 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.keyAtIndexD 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

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.min? Std.DTreeMap.Internal.Impl.leaf = none
• Std.DTreeMap.Internal.Impl.Const.min? (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) = some (k, v)
• Std.DTreeMap.Internal.Impl.Const.min? (Std.DTreeMap.Internal.Impl.inner size k v l r) = Std.DTreeMap.Internal.Impl.Const.min? l

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.min {α : Type u} {β : Type v} [Ord α] (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.min (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x_2 = (k, v)

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.min! Std.DTreeMap.Internal.Impl.leaf = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.min!" 738 13 "Map is empty"
• Std.DTreeMap.Internal.Impl.Const.min! (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) = (k, v)
• Std.DTreeMap.Internal.Impl.Const.min! (Std.DTreeMap.Internal.Impl.inner size k v l r) = Std.DTreeMap.Internal.Impl.Const.min! l

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.minD Std.DTreeMap.Internal.Impl.leaf x✝ = x✝
• Std.DTreeMap.Internal.Impl.Const.minD (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x✝ = (k, v)
• Std.DTreeMap.Internal.Impl.Const.minD (Std.DTreeMap.Internal.Impl.inner size k v l r) x✝ = Std.DTreeMap.Internal.Impl.Const.minD l x✝

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.max? Std.DTreeMap.Internal.Impl.leaf = none
• Std.DTreeMap.Internal.Impl.Const.max? (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) = some (k, v)
• Std.DTreeMap.Internal.Impl.Const.max? (Std.DTreeMap.Internal.Impl.inner size k v l r) = Std.DTreeMap.Internal.Impl.Const.max? r

@[irreducible]

def Std.DTreeMap.Internal.Impl.Const.max {α : Type u} {β : Type v} [Ord α] (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.max (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x_2 = (k, v)

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.max! Std.DTreeMap.Internal.Impl.leaf = panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.max!" 761 13 "Map is empty"
• Std.DTreeMap.Internal.Impl.Const.max! (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) = (k, v)
• Std.DTreeMap.Internal.Impl.Const.max! (Std.DTreeMap.Internal.Impl.inner size k v l r) = Std.DTreeMap.Internal.Impl.Const.max! r

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

Implementation detail of the tree map

Equations

• Std.DTreeMap.Internal.Impl.Const.maxD Std.DTreeMap.Internal.Impl.leaf x✝ = x✝
• Std.DTreeMap.Internal.Impl.Const.maxD (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x✝ = (k, v)
• Std.DTreeMap.Internal.Impl.Const.maxD (Std.DTreeMap.Internal.Impl.inner size k v l r) x✝ = Std.DTreeMap.Internal.Impl.Const.maxD r x✝

@[inline]

def Std.DTreeMap.Internal.Impl.Const.entryAtIdx {α : Type u} {β : Type v} [Ord α] (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} [Ord α] : (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} [Ord α] [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} [Ord α] : (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