Well-formedness proofs for raw tree maps #
This file contains well-formedness proofs about Std.Data.TreeMap.Raw.Basic. Most of the lemmas require
TransCmp cmp for the comparison function cmp.
theorem
Std.TreeMap.Raw.WF.insertIfNew
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{t : Raw α β cmp}
[TransCmp cmp]
{a : α}
{b : β}
(h : t.WF)
:
(t.insertIfNew a b).WF
theorem
Std.TreeMap.Raw.WF.ofList
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List (α × β)}
:
(Raw.ofList l cmp).WF
theorem
Std.TreeMap.Raw.WF.ofArray
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[TransCmp cmp]
{a : Array (α × β)}
:
(Raw.ofArray a cmp).WF
theorem
Std.TreeMap.Raw.WF.unitOfList
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{l : List α}
:
(Raw.unitOfList l cmp).WF
theorem
Std.TreeMap.Raw.WF.unitOfArray
{α : Type u}
{cmp : α → α → Ordering}
[TransCmp cmp]
{a : Array α}
:
(Raw.unitOfArray a cmp).WF
theorem
Std.TreeMap.Raw.WF.mergeWith
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{mergeFn : α → β → β → β}
{t₁ t₂ : Raw α β cmp}
(h : t₁.WF)
:
(Raw.mergeWith mergeFn t₁ t₂).WF