BestFirst
📁 Source: Mathlib/Deprecated/MLList/BestFirst.lean
Statistics
| Metric | Count |
|---|---|
| 19 | |
| Theorems | 0 |
| Total | 19 |
BestFirstNode
Definitions
| Name | Category | Theorems |
|---|---|---|
estimate 📖 | CompOp | — |
estimator 📖 | CompOp | — |
key 📖 | CompOp | — |
BestFirstQueue
Definitions
| Name | Category | Theorems |
|---|---|---|
ensureFirstIsBest 📖 | CompOp | — |
insertAndEject 📖 | CompOp | — |
pop 📖 | CompOp | — |
popWithBound 📖 | CompOp | — |
popWithPriority 📖 | CompOp | — |
toMLList 📖 | CompOp | — |
toMLListWithPriority 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
BestFirstNode 📖 | CompData | — |
BestFirstQueue 📖 | CompOp | — |
bestFirstSearch 📖 | CompOp | — |
bestFirstSearchCore 📖 | CompOp | — |
impl 📖 | CompOp | — |
implMaxDepth 📖 | CompOp | — |
instOrdBestFirstNode 📖 | CompOp | — |
instOrderBotEq 📖 | CompOp | — |
impl
Definitions
| Name | Category | Theorems |
|---|---|---|
go 📖 | CompOp | — |
---