Documentation Verification Report

Public

📁 Source: Aesop/Options/Public.lean

Statistics

Metric	Count
Definitions `applyHypsTransparency`, `assumptionTransparency`, `destructProductsTransparency`, `enableSimp`, `enableUnfold`, `introsTransparency?`, `maxGoals`, `maxNormIterations`, `maxRuleApplicationDepth`, `maxRuleApplications`, `maxSafePrefixRuleApplications`, `strategy`, `terminal`, `traceScript`, `useDefaultSimpSet`, `useSimpAll`, `warnOnNonterminal`, `collectStats`, `dynamicStructuring`, `generateScript`, `optimizedDynamicStructuring`, `statefulForward`, `file`, `applyIff`, `nonterminal`, `instBEqOptions`, `beq`, `instBEqStrategy`, `beq`, `instInhabitedOptions`, `default`, `instInhabitedStrategy`, `default`, `instReprOptions`, `repr`, `instReprStrategy`, `repr`	37
Theorems	0
Total	37

Aesop

Definitions

Name	Category	Theorems
`instBEqOptions` 📖	CompOp	—
`instBEqStrategy` 📖	CompOp	—
`instInhabitedOptions` 📖	CompOp	—
`instInhabitedStrategy` 📖	CompOp	—
`instReprOptions` 📖	CompOp	—
`instReprStrategy` 📖	CompOp	—

Aesop.Options

Definitions

Name	Category	Theorems
`applyHypsTransparency` 📖	CompOp	—
`assumptionTransparency` 📖	CompOp	—
`destructProductsTransparency` 📖	CompOp	—
`enableSimp` 📖	CompOp	—
`enableUnfold` 📖	CompOp	—
`introsTransparency?` 📖	CompOp	—
`maxGoals` 📖	CompOp	—
`maxNormIterations` 📖	CompOp	—
`maxRuleApplicationDepth` 📖	CompOp	—
`maxRuleApplications` 📖	CompOp	—
`maxSafePrefixRuleApplications` 📖	CompOp	—
`strategy` 📖	CompOp	—
`terminal` 📖	CompOp	—
`traceScript` 📖	CompOp	—
`useDefaultSimpSet` 📖	CompOp	—
`useSimpAll` 📖	CompOp	—
`warnOnNonterminal` 📖	CompOp	—

Aesop.aesop

Definitions

Name	Category	Theorems
`collectStats` 📖	CompOp	—

Aesop.aesop.dev

Definitions

Name	Category	Theorems
`dynamicStructuring` 📖	CompOp	—
`generateScript` 📖	CompOp	—
`optimizedDynamicStructuring` 📖	CompOp	—
`statefulForward` 📖	CompOp	—

Aesop.aesop.stats

Definitions

Name	Category	Theorems
`file` 📖	CompOp	—

Aesop.aesop.warn

Definitions

Name	Category	Theorems
`applyIff` 📖	CompOp	—
`nonterminal` 📖	CompOp	—

Aesop.instBEqOptions

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Aesop.instBEqStrategy

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

Aesop.instInhabitedOptions

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instInhabitedStrategy

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

Aesop.instReprOptions

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

Aesop.instReprStrategy

Definitions

Name	Category	Theorems
`repr` 📖	CompOp	—

---

← Back to Index