Documentation

Std.Data.DTreeMap.Internal.Queries

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 α β) :

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

Instances For

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 α β) :

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

Equations
theorem Std.DTreeMap.Internal.Impl.mem_iff_contains {α : Type u} {β : αType v} {x✝ : Ord α} {t : Impl α β} {k : α} :
theorem Std.DTreeMap.Internal.Impl.contains_iff_mem {α : Type u} {β : αType v} {x✝ : Ord α} {t : Impl α β} {k : α} :
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 α β) :

Returns true if the tree is empty.

Equations
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
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
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
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
def Std.DTreeMap.Internal.Impl.getKey? {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (k : α) :

Implementation detail of the tree map

Equations
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
def Std.DTreeMap.Internal.Impl.getKey! {α : Type u} {β : αType v} [Ord α] (t : Impl α β) (k : α) [Inhabited α] :
α

Implementation detail of the tree map

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

Implementation detail of the tree map

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

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

Equations
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
@[specialize #[]]
def Std.DTreeMap.Internal.Impl.foldlM {α : Type u} {β : αType v} {δ : Type w} {m : Type w → Type u_1} [Monad m] (f : δ(a : α) → β am δ) (init : δ) :
Impl α βm δ

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

Equations
@[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
@[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
@[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
@[inline]
def Std.DTreeMap.Internal.Impl.forM {α : Type u} {β : αType v} {m : Type u_1 → Type u_2} [Monad m] (f : (a : α) → β am PUnit) (t : Impl α β) :

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

Equations
@[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
@[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
@[inline]
def Std.DTreeMap.Internal.Impl.keysArray {α : Type u} {β : αType v} (t : Impl α β) :

Returns an Array of the keys in order.

Equations
@[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
@[inline]
def Std.DTreeMap.Internal.Impl.valuesArray {α : Type u} {β : Type v} (t : Impl α fun (x : α) => β) :

Returns an Array of the values in order.

Equations
@[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
@[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
@[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
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.minEntry? {α : Type u} {β : αType v} :
Impl α βOption ((a : α) × β a)

Implementation detail of the tree map

Equations
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.minEntry! {α : Type u} {β : αType v} [Inhabited ((a : α) × β a)] :
Impl α β(a : α) × β a

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.minEntryD {α : Type u} {β : αType v} :
Impl α β(a : α) × β a(a : α) × β a

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxEntry? {α : Type u} {β : αType v} :
Impl α βOption ((a : α) × β a)

Implementation detail of the tree map

Equations
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxEntry! {α : Type u} {β : αType v} [Inhabited ((a : α) × β a)] :
Impl α β(a : α) × β a

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxEntryD {α : Type u} {β : αType v} :
Impl α β(a : α) × β a(a : α) × β a

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.minKey? {α : Type u} {β : αType v} :
Impl α βOption α

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.minKey {α : Type u} {β : αType v} (t : Impl α β) (h : t.isEmpty = false) :
α

Implementation detail of the tree map

Equations
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.minKeyD {α : Type u} {β : αType v} :
Impl α βαα

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxKey? {α : Type u} {β : αType v} :
Impl α βOption α

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxKey {α : Type u} {β : αType v} (t : Impl α β) (h : t.isEmpty = false) :
α

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.maxKeyD {α : Type u} {β : αType v} :
Impl α βαα

Implementation detail of the tree map

Equations
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 α βNatOption ((a : α) × β a)

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
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 α βNatOption α

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getEntryLT?.go {α : Type u} {β : αType v} [Ord α] (k : α) (best : Option ((a : α) × β a)) :
Impl α βOption ((a : α) × β a)
Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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
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
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
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
@[inline]
def Std.DTreeMap.Internal.Impl.getKeyGE? {α : Type u} {β : αType v} [Ord α] (k : α) :
Impl α βOption α

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
def Std.DTreeMap.Internal.Impl.getKeyLT?.go {α : Type u} {β : αType v} [Ord α] (k : α) (best : Option α) :
Impl α βOption α
Equations
@[inline]
def Std.DTreeMap.Internal.Impl.getKeyGE! {α : Type u} {β : αType v} [Ord α] [Inhabited α] (k : α) (t : Impl α β) :
α

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
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
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
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
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
@[irreducible]
def Std.DTreeMap.Internal.Impl.Const.minEntry? {α : Type u} {β : Type v} :
(Impl α fun (x : α) => β)Option (α × β)

Implementation detail of the tree map

Equations
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.Const.minEntry! {α : Type u} {β : Type v} [Inhabited (α × β)] :
(Impl α fun (x : α) => β)α × β

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.Const.minEntryD {α : Type u} {β : Type v} :
(Impl α fun (x : α) => β)α × βα × β

Implementation detail of the tree map

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

Implementation detail of the tree map

Equations
@[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
@[irreducible]
def Std.DTreeMap.Internal.Impl.Const.maxEntry! {α : Type u} {β : Type v} [Inhabited (α × β)] :
(Impl α fun (x : α) => β)α × β

Implementation detail of the tree map

Equations
@[irreducible]
def Std.DTreeMap.Internal.Impl.Const.maxEntryD {α : Type u} {β : Type v} :
(Impl α fun (x : α) => β)α × βα × β

Implementation detail of the tree map

Equations
@[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 : α) => β)NatOption (α × β)

Implementation detail of the tree map

Equations
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
@[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
def Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) :
(Impl α fun (x : α) => β)Option (α × β)
Equations
@[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
def Std.DTreeMap.Internal.Impl.Const.getEntryGT?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) :
(Impl α fun (x : α) => β)Option (α × β)
Equations
@[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
def Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) :
(Impl α fun (x : α) => β)Option (α × β)
Equations
@[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
def Std.DTreeMap.Internal.Impl.Const.getEntryLT?.go {α : Type u} {β : Type v} [Ord α] (k : α) (best : Option (α × β)) :
(Impl α fun (x : α) => β)Option (α × β)
Equations
@[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
@[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
@[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
@[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
@[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
@[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
@[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
@[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
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
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
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
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