Basic

📁 Source: Batteries/Data/BinomialHeap/Basic.lean

Statistics

Metric	Count
Definitions FindMin, rank, before, next, node, val, Heap, findMin, deleteMin, findMin, fold, foldM, foldTree, foldTreeM, head?, headD, isEmpty, length, merge, rankGT, realSize, singleton, size, tail, tail?, toArray, toArrayUnordered, toList, toListUnordered, HeapNode, foldTreeM, rank, rankTR, go, realSize, singleton, toHeap, go, combine, instDecidableRankGT, instReprHeap, repr, instReprHeapNode, repr, deleteMin, empty, fold, foldM, forIn, head!, head?, headI, insert, instEmptyCollection, instForInOfMonad, instInhabited, instStream, isEmpty, merge, ofArray, ofList, singleton, size, tail, tail?, toArray, toArrayUnordered, toList, toListUnordered, mkBinomialHeap	70
Theorems before, next, node, deleteMin, merge, merge', nil, of_le, of_rankGT, rankGT, singleton, tail, tail?, of_le, realSize_deleteMin, realSize_merge, realSize_tail, realSize_tail?, rank_eq, toHeap, rankTR_eq, realSize_toHeap	22
Total	92

Batteries

Definitions

Name	Category	Theorems
mkBinomialHeap 📖	CompOp	—

Batteries.BinomialHeap

Definitions

Name	Category	Theorems
deleteMin 📖	CompOp	—
empty 📖	CompOp	—
fold 📖	CompOp	—
foldM 📖	CompOp	—
forIn 📖	CompOp	—
head! 📖	CompOp	—
head? 📖	CompOp	—
headI 📖	CompOp	—
insert 📖	CompOp	—
instEmptyCollection 📖	CompOp	—
instForInOfMonad 📖	CompOp	—
instInhabited 📖	CompOp	—
instStream 📖	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.BinomialHeap.Imp

Definitions

Name	Category	Theorems
FindMin 📖	CompData	—
Heap 📖	CompData	1 math math: Heap.deleteMin_fst
HeapNode 📖	CompData	—
combine 📖	CompOp	—
instDecidableRankGT 📖	CompOp	—
instReprHeap 📖	CompOp	—
instReprHeapNode 📖	CompOp	—

Batteries.BinomialHeap.Imp.FindMin

Definitions

Name	Category	Theorems
before 📖	CompOp	1 math math: WF.before
next 📖	CompOp	1 math math: WF.next
node 📖	CompOp	1 math math: WF.node
val 📖	CompOp	2 math math: Batteries.BinomialHeap.Imp.Heap.findMin_val, WF.node

Batteries.BinomialHeap.Imp.FindMin.WF

Definitions

Name	Category	Theorems
rank 📖	CompOp	2 math math: next, node

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
before 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF rank	Batteries.BinomialHeap.Imp.FindMin.before	—	—
next 📖	mathematical	—	Batteries.BinomialHeap.Imp.Heap.WF rank Batteries.BinomialHeap.Imp.FindMin.next	—	—
node 📖	mathematical	—	Batteries.BinomialHeap.Imp.HeapNode.WF Batteries.BinomialHeap.Imp.FindMin.val Batteries.BinomialHeap.Imp.FindMin.node rank	—	—

Batteries.BinomialHeap.Imp.Heap

Definitions

Name	Category	Theorems
deleteMin 📖	CompOp	1 math math: deleteMin_fst
findMin 📖	CompOp	1 math math: findMin_val
fold 📖	CompOp	—
foldM 📖	CompOp	—
foldTree 📖	CompOp	—
foldTreeM 📖	CompOp	—
head? 📖	CompOp	1 math math: deleteMin_fst
headD 📖	CompOp	1 math math: findMin_val
isEmpty 📖	CompOp	—
length 📖	CompOp	—
merge 📖	CompOp	3 math math: realSize_merge, WF.merge', WF.merge
rankGT 📖	MathDef	2 math math: WF.merge', WF.rankGT
realSize 📖	CompOp	6 math math: realSize_merge, realSize_tail, realSize_tail?, WF.size_eq, Batteries.BinomialHeap.Imp.HeapNode.realSize_toHeap, realSize_deleteMin
singleton 📖	CompOp	1 math math: WF.singleton
size 📖	CompOp	1 math math: WF.size_eq
tail 📖	CompOp	2 math math: realSize_tail, WF.tail
tail? 📖	CompOp	—
toArray 📖	CompOp	—
toArrayUnordered 📖	CompOp	—
toList 📖	CompOp	—
toListUnordered 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realSize_deleteMin 📖	mathematical	deleteMin Batteries.BinomialHeap.Imp.Heap	realSize	—	realSize.eq_2 realSize_merge Batteries.BinomialHeap.Imp.HeapNode.realSize_toHeap
realSize_merge 📖	mathematical	—	realSize merge	—	—
realSize_tail 📖	mathematical	—	realSize tail	—	realSize_tail?
realSize_tail? 📖	mathematical	tail? Batteries.BinomialHeap.Imp.Heap	realSize	—	realSize_deleteMin

Batteries.BinomialHeap.Imp.Heap.WF

Definitions

Name	Category	Theorems
findMin 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deleteMin 📖	—	Batteries.BinomialHeap.Imp.Heap.WF Batteries.BinomialHeap.Imp.Heap.deleteMin Batteries.BinomialHeap.Imp.Heap	—	—	of_le merge Batteries.BinomialHeap.Imp.HeapNode.WF.toHeap
merge 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF	Batteries.BinomialHeap.Imp.Heap.merge	—	merge'
merge' 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF	Batteries.BinomialHeap.Imp.Heap.merge Batteries.BinomialHeap.Imp.Heap.rankGT	—	—
nil 📖	mathematical	—	Batteries.BinomialHeap.Imp.Heap.WF Batteries.BinomialHeap.Imp.Heap.nil	—	—
of_le 📖	—	Batteries.BinomialHeap.Imp.Heap.WF	—	—	—
of_rankGT 📖	—	Batteries.BinomialHeap.Imp.Heap.rankGT Batteries.BinomialHeap.Imp.Heap.WF	—	—	—
rankGT 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF	Batteries.BinomialHeap.Imp.Heap.rankGT	—	—
singleton 📖	mathematical	—	Batteries.BinomialHeap.Imp.Heap.WF Batteries.BinomialHeap.Imp.Heap.singleton	—	—
tail 📖	mathematical	Batteries.BinomialHeap.Imp.Heap.WF	Batteries.BinomialHeap.Imp.Heap.tail	—	nil tail?
tail? 📖	—	Batteries.BinomialHeap.Imp.Heap.WF Batteries.BinomialHeap.Imp.Heap.tail? Batteries.BinomialHeap.Imp.Heap	—	—	deleteMin

Batteries.BinomialHeap.Imp.Heap.rankGT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_le 📖	—	Batteries.BinomialHeap.Imp.Heap.rankGT	—	—	—

Batteries.BinomialHeap.Imp.HeapNode

Definitions

Name	Category	Theorems
foldTreeM 📖	CompOp	—
rank 📖	CompOp	2 math math: WF.rank_eq, rankTR_eq
rankTR 📖	CompOp	1 math math: rankTR_eq
realSize 📖	CompOp	2 math math: WF.realSize_eq, realSize_toHeap
singleton 📖	CompOp	—
toHeap 📖	CompOp	2 math math: WF.toHeap, realSize_toHeap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rankTR_eq 📖	mathematical	—	rankTR rank	—	—
realSize_toHeap 📖	mathematical	—	Batteries.BinomialHeap.Imp.Heap.realSize toHeap realSize	—	—

Batteries.BinomialHeap.Imp.HeapNode.WF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rank_eq 📖	mathematical	Batteries.BinomialHeap.Imp.HeapNode.WF	Batteries.BinomialHeap.Imp.HeapNode.rank	—	—
toHeap 📖	mathematical	Batteries.BinomialHeap.Imp.HeapNode.WF	Batteries.BinomialHeap.Imp.Heap.WF Batteries.BinomialHeap.Imp.HeapNode.toHeap	—	—

Batteries.BinomialHeap.Imp.HeapNode.rankTR

Definitions

Name	Category	Theorems
go 📖	CompOp	—

Batteries.BinomialHeap.Imp.HeapNode.toHeap

Definitions

Name	Category	Theorems
go 📖	CompOp	—

Batteries.BinomialHeap.Imp.instReprHeap

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

Batteries.BinomialHeap.Imp.instReprHeapNode

Definitions

Name	Category	Theorems
repr 📖	CompOp	—

---

← Back to Index