PairingHeap

📁 Source: Batteries/Data/PairingHeap.lean

Statistics

Metric	Count
Definitions PairingHeap, deleteMin, empty, head!, head?, headI, insert, instInhabited, isEmpty, merge, ofArray, ofList, singleton, size, tail, tail?, toArray, toArrayUnordered, toList, toListUnordered, Heap, NoSibling, NodeWF, combine, deleteMin, fold, foldM, foldTree, foldTreeM, head?, headD, isEmpty, merge, singleton, size, tail, tail?, toArray, toArrayUnordered, toList, toListUnordered, instDecidableNoSibling, instReprHeap, repr, mkPairingHeap	45
Theorems combine, deleteMin, merge, merge_node, singleton, tail, tail?, deleteMin_fst, noSibling_combine, noSibling_deleteMin, noSibling_merge, noSibling_tail, noSibling_tail?, size_combine, size_deleteMin, size_deleteMin_lt, size_merge, size_merge_node, size_tail, size_tail?, size_tail?_lt	21
Total	66

Batteries

Definitions

Name	Category	Theorems
PairingHeap 📖	CompOp	—
mkPairingHeap 📖	CompOp	—

Batteries.PairingHeap

Definitions

Name	Category	Theorems
deleteMin 📖	CompOp	—
empty 📖	CompOp	—
head! 📖	CompOp	—
head? 📖	CompOp	—
headI 📖	CompOp	—
insert 📖	CompOp	—
instInhabited 📖	CompOp	—
isEmpty 📖	CompOp	—
merge 📖	CompOp	—
ofArray 📖	CompOp	—
ofList 📖	CompOp	—
singleton 📖	CompOp	—
size 📖	CompOp	—
tail 📖	CompOp	—
tail? 📖	CompOp	—
toArray 📖	CompOp	—
toArrayUnordered 📖	CompOp	—
toList 📖	CompOp	—
toListUnordered 📖	CompOp	—

Batteries.PairingHeapImp

Definitions

Name	Category	Theorems
Heap 📖	CompData	1 math math: Heap.deleteMin_fst
instDecidableNoSibling 📖	CompOp	—
instReprHeap 📖	CompOp	—

Batteries.PairingHeapImp.Heap

Definitions

Name	Category	Theorems
NoSibling 📖	CompData	5 math math: noSibling_deleteMin, noSibling_tail, noSibling_tail?, noSibling_merge, noSibling_combine
NodeWF 📖	MathDef	—
combine 📖	CompOp	3 math math: WF.combine, size_combine, noSibling_combine
deleteMin 📖	CompOp	1 math math: deleteMin_fst
fold 📖	CompOp	—
foldM 📖	CompOp	—
foldTree 📖	CompOp	—
foldTreeM 📖	CompOp	—
head? 📖	CompOp	1 math math: deleteMin_fst
headD 📖	CompOp	—
isEmpty 📖	CompOp	—
merge 📖	CompOp	5 math math: WF.merge, size_merge_node, size_merge, noSibling_merge, WF.merge_node
singleton 📖	CompOp	1 math math: WF.singleton
size 📖	CompOp	8 math math: size_tail?, size_tail?_lt, size_merge_node, size_merge, size_tail, size_deleteMin_lt, size_deleteMin, size_combine
tail 📖	CompOp	3 math math: noSibling_tail, WF.tail, size_tail
tail? 📖	CompOp	—
toArray 📖	CompOp	—
toArrayUnordered 📖	CompOp	—
toList 📖	CompOp	—
toListUnordered 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deleteMin_fst 📖	mathematical	—	Batteries.PairingHeapImp.Heap deleteMin head?	—	—
noSibling_combine 📖	mathematical	—	NoSibling combine	—	combine.eq_def noSibling_merge
noSibling_deleteMin 📖	mathematical	deleteMin Batteries.PairingHeapImp.Heap	NoSibling	—	noSibling_combine
noSibling_merge 📖	mathematical	—	NoSibling merge	—	—
noSibling_tail 📖	mathematical	—	NoSibling tail	—	noSibling_tail?
noSibling_tail? 📖	mathematical	tail? Batteries.PairingHeapImp.Heap	NoSibling	—	noSibling_deleteMin
size_combine 📖	mathematical	—	size combine	—	combine.eq_def size_merge noSibling_merge noSibling_combine size_merge_node
size_deleteMin 📖	mathematical	NoSibling deleteMin Batteries.PairingHeapImp.Heap	size	—	size_combine size.eq_2 size.eq_1
size_deleteMin_lt 📖	mathematical	deleteMin Batteries.PairingHeapImp.Heap	size	—	size_combine
size_merge 📖	mathematical	NoSibling	size merge	—	—
size_merge_node 📖	mathematical	—	size merge node	—	—
size_tail 📖	mathematical	NoSibling	size tail	—	size_tail?
size_tail? 📖	mathematical	NoSibling tail? Batteries.PairingHeapImp.Heap	size	—	size_deleteMin
size_tail?_lt 📖	mathematical	tail? Batteries.PairingHeapImp.Heap	size	—	size_deleteMin_lt

Batteries.PairingHeapImp.Heap.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
combine 📖	mathematical	Batteries.PairingHeapImp.Heap.NodeWF	Batteries.PairingHeapImp.Heap.WF Batteries.PairingHeapImp.Heap.combine	—	merge merge_node
deleteMin 📖	—	Batteries.PairingHeapImp.Heap.WF Batteries.PairingHeapImp.Heap.deleteMin Batteries.PairingHeapImp.Heap	—	—	combine
merge 📖	mathematical	Batteries.PairingHeapImp.Heap.WF	Batteries.PairingHeapImp.Heap.merge	—	merge_node
merge_node 📖	mathematical	Batteries.PairingHeapImp.Heap.NodeWF	Batteries.PairingHeapImp.Heap.WF Batteries.PairingHeapImp.Heap.merge Batteries.PairingHeapImp.Heap.node	—	Batteries.TotalBLE.total
singleton 📖	mathematical	—	Batteries.PairingHeapImp.Heap.WF Batteries.PairingHeapImp.Heap.singleton	—	—
tail 📖	mathematical	Batteries.PairingHeapImp.Heap.WF	Batteries.PairingHeapImp.Heap.tail	—	tail?
tail? 📖	—	Batteries.PairingHeapImp.Heap.WF Batteries.PairingHeapImp.Heap.tail? Batteries.PairingHeapImp.Heap	—	—	deleteMin

Batteries.PairingHeapImp.instReprHeap

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

---

← Back to Index