Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `heapSort`, `toBinaryHeap`, `arr`, `decreaseKey`, `empty`, `extractMax`, `get`, `heapifyDown`, `heapifyUp`, `increaseKey`, `insert`, `insertExtractMax`, `instEmptyCollection`, `instInhabited`, `max`, `mkHeap`, `popMax`, `replaceMax`, `singleton`, `size`, `toBinaryHeap`	21
Theorems `size_insert`, `size_popMax`, `size_pos_of_max`	3
Total	24

Array

Definitions

Name	Category	Theorems
`heapSort` 📖	CompOp	—
`toBinaryHeap` 📖	CompOp	—

Batteries.BinaryHeap

Definitions

Name	Category	Theorems
`arr` 📖	CompOp	—
`decreaseKey` 📖	CompOp	—
`empty` 📖	CompOp	—
`extractMax` 📖	CompOp	—
`get` 📖	CompOp	—
`heapifyDown` 📖	CompOp	—
`heapifyUp` 📖	CompOp	—
`increaseKey` 📖	CompOp	—
`insert` 📖	CompOp	1 math math: `size_insert`
`insertExtractMax` 📖	CompOp	—
`instEmptyCollection` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`max` 📖	CompOp	—
`mkHeap` 📖	CompOp	—
`popMax` 📖	CompOp	1 math math: `size_popMax`
`replaceMax` 📖	CompOp	—
`singleton` 📖	CompOp	—
`size` 📖	CompOp	3 math math: `size_insert`, `size_pos_of_max`, `size_popMax`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`size_insert` 📖	mathematical	—	`size` `insert`	—	—
`size_popMax` 📖	mathematical	—	`size` `popMax`	—	—
`size_pos_of_max` 📖	mathematical	`max`	`size`	—	—

Batteries.Vector

Definitions

Name	Category	Theorems
`toBinaryHeap` 📖	CompOp	—

---

← Back to Index