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.instCoeTypeForall {α : Type u} : Coe (Type v) (α → Type v)

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.

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.

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

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)

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.

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.

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.

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.

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.

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

Returns the entry (key-value pair) for the key k, or none if such a key does not exist.

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

Returns the entry (key-value pair) for the key k.

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

Returns the entry (key-value pair) for the key k, or panics if such a key does not exist.

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

Returns the entry (key-value pair) for the key k, or fallback if such a key does not exist.

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

Implementation detail of the tree map

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

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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.

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.

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

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

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.

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

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

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

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

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

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

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

instance Std.DTreeMap.Internal.Impl.instForInSigmaOfMonad {α : Type u} {β : α → Type v} {m : Type w → Type w'} [Monad m] : ForIn m (Impl α β) ((a : α) × β a)

@[inline]

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

Implementation detail.

@[inline]

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

Implementation detail.

@[inline]

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

Returns a List of the keys in order.

@[inline]

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

Returns an Array of the keys in order.

@[inline]

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

Returns a List of the values in order.

@[inline]

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

Returns an Array of the values in order.

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

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

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

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

@[irreducible]

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

Implementation detail of the tree map

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

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

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

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

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

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

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

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

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

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

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

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

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

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

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

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

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

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

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

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

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

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

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

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

@[irreducible]

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

Implementation detail of the tree map

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

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

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

@[irreducible]

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

Implementation detail of the tree map

@[irreducible]

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

Implementation detail of the tree map

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

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

@[inline]

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

Implementation detail of the tree map

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

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

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

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

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

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

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

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

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

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

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

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

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