@[simp]

theorem Std.ExtTreeMap.maxEntry?_empty {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] : ∅.maxEntry? = none

The empty map has no maximum entry.

def Std.ExtTreeMap.foldl₂ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {cmp : α → α → Ordering} [TransCmp cmp] (f : δ → α → Option β → Option γ → δ) (init : δ) (left : ExtTreeMap α β cmp) (right : ExtTreeMap α γ cmp) : δ

Joint ordered fold over two maps in increasing comparator order.

The callback sees some exactly on the sides that contain a comparator-equivalent key; at a shared entry it receives the left map's key representative. The implementation performs linear merge work after materializing the two ordered streams.

Equations

• Std.ExtTreeMap.foldl₂ f init left right = Std.ExtTreeMap.foldl₂.mergeFold f init left.toList right.toList

@[irreducible]

def Std.ExtTreeMap.foldl₂.mergeFold {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {cmp : α → α → Ordering} (f : δ → α → Option β → Option γ → δ) : δ → List (α × β) → List (α × γ) → δ

Joint-fold worker. Nesting keeps it out of the top-level Std.ExtTreeMap namespace, but exposure makes it a public constant. Callers must supply sorted, comparator-distinct streams, as ExtTreeMap.toList produces; behavior on other lists is unspecified.

Equations

• One or more equations did not get rendered due to their size.
• Std.ExtTreeMap.foldl₂.mergeFold f a✝¹ [] a✝ = List.foldl (fun (acc : δ) (entry : α × γ) => f acc entry.fst none (some entry.snd)) a✝¹ a✝
• Std.ExtTreeMap.foldl₂.mergeFold f a✝¹ a✝ [] = List.foldl (fun (acc : δ) (entry : α × β) => f acc entry.fst (some entry.snd) none) a✝¹ a✝

def Std.ExtTreeMap.mergeValue? {α : Type u} {β : Type v} (f : α → β → β → Option β) (key : α) : Option β → Option β → Option β

Result for one key in a deletion-capable merge.

Equations

• Std.ExtTreeMap.mergeValue? f key none x✝ = x✝
• Std.ExtTreeMap.mergeValue? f key x✝ none = x✝
• Std.ExtTreeMap.mergeValue? f key (some left) (some right) = f key left right

def Std.ExtTreeMap.mergeWith? {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (f : α → β → β → Option β) (left right : ExtTreeMap α β cmp) : ExtTreeMap α β cmp

Merge two maps, allowing a collision to delete its key.

Left-only and right-only entries are retained unchanged. The smaller map is folded into the larger map, so the operation performs O(min(m,n) * log(max(m,n))) tree work. The collision callback always receives the left value before the right value, independent of which map is smaller. LawfulEqCmp makes comparator-equivalent keys propositionally equal, so the choice of the larger map cannot observably change the stored collision key.

Equations

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

@[simp]

theorem Std.ExtTreeMap.getElem?_mergeWith? {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (f : α → β → β → Option β) (left right : ExtTreeMap α β cmp) (key : α) : (mergeWith? f left right)[key]? = mergeValue? f key left[key]? right[key]?

Lookup specification for a deletion-capable merge.

@[simp]

theorem Std.ExtTreeMap.foldl₂_empty_left {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {cmp : α → α → Ordering} [TransCmp cmp] (f : δ → α → Option β → Option γ → δ) (init : δ) (right : ExtTreeMap α γ cmp) : foldl₂ f init ∅ right = foldl (fun (acc : δ) (key : α) (value : γ) => f acc key none (some value)) init right

@[simp]

theorem Std.ExtTreeMap.foldl₂_empty_right {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {cmp : α → α → Ordering} [TransCmp cmp] (f : δ → α → Option β → Option γ → δ) (init : δ) (left : ExtTreeMap α β cmp) : foldl₂ f init left ∅ = foldl (fun (acc : δ) (key : α) (value : β) => f acc key (some value) none) init left

@[simp]

theorem Std.ExtTreeMap.mergeWith?_empty_left {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (f : α → β → β → Option β) (right : ExtTreeMap α β cmp) : mergeWith? f ∅ right = right

@[simp]

theorem Std.ExtTreeMap.mergeWith?_empty_right {α : Type u} {β : Type v} {cmp : α → α → Ordering} [TransCmp cmp] [LawfulEqCmp cmp] (f : α → β → β → Option β) (left : ExtTreeMap α β cmp) : mergeWith? f left ∅ = left