# Low-level implementation of the size-bounded tree #

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

source
def Std.DTreeMap.Internal.Impl.instCoeTypeForall {α : Type u} :
Coe (Type v) (α → Type v)
Equations

- Std.DTreeMap.Internal.Impl.instCoeTypeForall = { coe := fun (γ : Type ?u.10) (x : α) => γ }

Instances For

source
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

Instances For

source
def Std.DTreeMap.Internal.Impl.«term_~m_» :
Lean.TrailingParserDescr

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

Equations

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

Instances For

source
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

Instances For

source
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 }

source
theorem Std.DTreeMap.Internal.Impl.mem_iff_contains {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {k : α} :
k ∈ t ↔ contains k t = true
source
theorem Std.DTreeMap.Internal.Impl.contains_iff_mem {α : Type u} {β : α → Type v} {x✝ : Ord α} {t : Impl α β} {k : α} :
contains k t = true ↔ k ∈ t
source
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))

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

Instances For

source
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)

Instances For

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

Returns the value for the key `k`.

Equations

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

Instances For

source
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!" 102 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

Instances For

source
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

Instances For

source
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'

Instances For

source
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'

Instances For

source
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!" 141 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'

Instances For

source
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'

Instances For

source
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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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

Instances For

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

Instances For

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

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

Equations

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

Instances For

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

Instances For

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

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

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Returns an `Array` of the keys in order.

Equations

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

Instances For

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

Instances For

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

Returns an `Array` of the values in order.

Equations

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

Instances For

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

Instances For

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

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

Equations

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

Instances For

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

Instances For

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

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

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

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

Equations

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

Instances For

source
@[irreducible]
def Std.DTreeMap.Internal.Impl.minKeyD {α : Type u} {β : α → Type v} :
Impl α β → α → α

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

source
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.

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

source
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.

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

source
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.

Instances For

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

Implementation detail of the tree map

Equations

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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For