Documentation Verification Report

SearchM

📁 Source: Aesop/Search/SearchM.lean

Statistics

Metric	Count
Definitions `NormSimpContext`, `configStx?`, `enabled`, `simprocs`, `toContext`, `useHyps`, `SearchM`, `Context`, `normSimpContext`, `options`, `ruleSet`, `iteration`, `maxRuleApplicationDepthReached`, `queue`, `instInhabited`, `instInhabitedState`, `default`, `instMonad`, `instMonadLiftTreeM`, `instMonadReaderContext`, `instMonadRef`, `instMonadStateState`, `run`, `run'`, `enqueueGoals`, `getIteration`, `getTree`, `incrementIteration`, `instInhabitedNormSimpContext`, `default`, `modifyTree`, `popGoal?`, `setMaxRuleApplicationDepthReached`, `setTree`, `wasMaxRuleApplicationDepthReached`	35
Theorems `instNonemptyContext`	1
Total	36

Aesop

Definitions

Name	Category	Theorems
`NormSimpContext` 📖	CompData	—
`SearchM` 📖	CompOp	—
`enqueueGoals` 📖	CompOp	—
`getIteration` 📖	CompOp	—
`getTree` 📖	CompOp	—
`incrementIteration` 📖	CompOp	—
`instInhabitedNormSimpContext` 📖	CompOp	—
`modifyTree` 📖	CompOp	—
`popGoal?` 📖	CompOp	—
`setMaxRuleApplicationDepthReached` 📖	CompOp	—
`setTree` 📖	CompOp	—
`wasMaxRuleApplicationDepthReached` 📖	CompOp	—

Aesop.NormSimpContext

Definitions

Name	Category	Theorems
`configStx?` 📖	CompOp	—
`enabled` 📖	CompOp	—
`simprocs` 📖	CompOp	—
`toContext` 📖	CompOp	—
`useHyps` 📖	CompOp	—

Aesop.SearchM

Definitions

Name	Category	Theorems
`Context` 📖	CompData	1 math math: `instNonemptyContext`
`instInhabited` 📖	CompOp	—
`instInhabitedState` 📖	CompOp	—
`instMonad` 📖	CompOp	—
`instMonadLiftTreeM` 📖	CompOp	—
`instMonadReaderContext` 📖	CompOp	—
`instMonadRef` 📖	CompOp	—
`instMonadStateState` 📖	CompOp	—
`run` 📖	CompOp	—
`run'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonemptyContext` 📖	mathematical	—	`Context`	—	—

Aesop.SearchM.Context

Definitions

Name	Category	Theorems
`normSimpContext` 📖	CompOp	—
`options` 📖	CompOp	—
`ruleSet` 📖	CompOp	—

Aesop.SearchM.State

Definitions

Name	Category	Theorems
`iteration` 📖	CompOp	—
`maxRuleApplicationDepthReached` 📖	CompOp	—
`queue` 📖	CompOp	—

Aesop.SearchM.instInhabitedState

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedNormSimpContext

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index