Documentation Verification Report

Declarations

📁 Source: Mathlib/Tactic/TacticAnalysis/Declarations.lean

Statistics

Metric	Count
Definitions `grindReplacementWith`, `introMerge`, `mergeWithGrind`, `rwMerge`, `terminalReplacement`, `terminalToGrind`, `tryAtEachStepCore`, `tryAtEachStepFromEnvImpl`, `tryAtEachStepFromStrings`, `verifyTryThisSuggestions`, `linarithToGrindRegressions`, `introMerge`, `mergeWithGrind`, `omegaToLia`, `linarithToGrind`, `omegaToLia`, `ringToGrind`, `rwMerge`, `terminalToGrind`, `fraction`, `selfReplacements`, `showTiming`, `tryAtEachStepAesop`, `tryAtEachStepFromEnv`, `tryAtEachStepGrind`, `tryAtEachStepGrindSuggestions`, `tryAtEachStepSimpAll`, `tryAtEachStepSimpAllSuggestions`, `verifyGrind`, `verifyGrindSuggestions`, `omegaToLia`, `omegaToLiaRegressions`, `ringToGrindRegressions`, `tryAtEachStepAesop`, `tryAtEachStepFromEnv`, `tryAtEachStepGrind`, `tryAtEachStepGrindSuggestions`, `tryAtEachStepSimpAll`, `tryAtEachStepSimpAllSuggestions`, `verifyGrind`, `verifyGrindSuggestions`	41
Theorems	0
Total	41

Mathlib.TacticAnalysis

Definitions

Name	Category	Theorems
`grindReplacementWith` 📖	CompOp	—
`introMerge` 📖	CompOp	—
`mergeWithGrind` 📖	CompOp	—
`rwMerge` 📖	CompOp	—
`terminalReplacement` 📖	CompOp	—
`terminalToGrind` 📖	CompOp	—
`tryAtEachStepCore` 📖	CompOp	—
`tryAtEachStepFromEnvImpl` 📖	CompOp	—
`tryAtEachStepFromStrings` 📖	CompOp	—
`verifyTryThisSuggestions` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`linarithToGrindRegressions` 📖	CompOp	—
`omegaToLia` 📖	CompOp	—
`omegaToLiaRegressions` 📖	CompOp	—
`ringToGrindRegressions` 📖	CompOp	—
`tryAtEachStepAesop` 📖	CompOp	—
`tryAtEachStepFromEnv` 📖	CompOp	—
`tryAtEachStepGrind` 📖	CompOp	—
`tryAtEachStepGrindSuggestions` 📖	CompOp	—
`tryAtEachStepSimpAll` 📖	CompOp	—
`tryAtEachStepSimpAllSuggestions` 📖	CompOp	—
`verifyGrind` 📖	CompOp	—
`verifyGrindSuggestions` 📖	CompOp	—

linter.tacticAnalysis

Definitions

Name	Category	Theorems
`introMerge` 📖	CompOp	—
`mergeWithGrind` 📖	CompOp	—
`omegaToLia` 📖	CompOp	—
`rwMerge` 📖	CompOp	—
`terminalToGrind` 📖	CompOp	—
`tryAtEachStepAesop` 📖	CompOp	—
`tryAtEachStepFromEnv` 📖	CompOp	—
`tryAtEachStepGrind` 📖	CompOp	—
`tryAtEachStepGrindSuggestions` 📖	CompOp	—
`tryAtEachStepSimpAll` 📖	CompOp	—
`tryAtEachStepSimpAllSuggestions` 📖	CompOp	—
`verifyGrind` 📖	CompOp	—
`verifyGrindSuggestions` 📖	CompOp	—

linter.tacticAnalysis.regressions

Definitions

Name	Category	Theorems
`linarithToGrind` 📖	CompOp	—
`omegaToLia` 📖	CompOp	—
`ringToGrind` 📖	CompOp	—

linter.tacticAnalysis.tryAtEachStep

Definitions

Name	Category	Theorems
`fraction` 📖	CompOp	—
`selfReplacements` 📖	CompOp	—
`showTiming` 📖	CompOp	—

---

← Back to Index