Documentation Verification Report

Queue

📁 Source: Aesop/Search/Queue.lean

Statistics

Metric	Count
Definitions `BestFirstQueue`, `ActiveGoal`, `addedInIteration`, `goal`, `lastExpandedInIteration`, `le`, `ofGoalRef`, `priority`, `addGoals`, `init`, `popGoal`, `FIFOQueue`, `addGoals`, `goals`, `init`, `instQueue`, `popGoal`, `pos`, `LIFOQueue`, `addGoals`, `goals`, `init`, `instQueue`, `popGoal`, `queue`, `Queue`, `Queue`, `instQueueBestFirstQueue`	28
Theorems	0
Total	28

Aesop

Definitions

Name	Category	Theorems
`BestFirstQueue` 📖	CompOp	—
`FIFOQueue` 📖	CompData	—
`LIFOQueue` 📖	CompData	—
`Queue` 📖	CompData	—
`instQueueBestFirstQueue` 📖	CompOp	—

Aesop.BestFirstQueue

Definitions

Name	Category	Theorems
`ActiveGoal` 📖	CompData	—
`addGoals` 📖	CompOp	—
`init` 📖	CompOp	—
`popGoal` 📖	CompOp	—

Aesop.BestFirstQueue.ActiveGoal

Definitions

Name	Category	Theorems
`addedInIteration` 📖	CompOp	—
`goal` 📖	CompOp	—
`lastExpandedInIteration` 📖	CompOp	—
`le` 📖	CompOp	—
`ofGoalRef` 📖	CompOp	—
`priority` 📖	CompOp	—

Aesop.FIFOQueue

Definitions

Name	Category	Theorems
`addGoals` 📖	CompOp	—
`goals` 📖	CompOp	—
`init` 📖	CompOp	—
`instQueue` 📖	CompOp	—
`popGoal` 📖	CompOp	—
`pos` 📖	CompOp	—

Aesop.LIFOQueue

Definitions

Name	Category	Theorems
`addGoals` 📖	CompOp	—
`goals` 📖	CompOp	—
`init` 📖	CompOp	—
`instQueue` 📖	CompOp	—
`popGoal` 📖	CompOp	—

Aesop.Options

Definitions

Name	Category	Theorems
`queue` 📖	CompOp	—

Aesop.Stateful

Definitions

Name	Category	Theorems
`Queue` 📖	CompOp	—

---

← Back to Index