Tauto

📁 Source: Mathlib/Tactic/Tauto.lean

Statistics

Metric	Count
Definitions DistribNotState, currentGoal, fvars, casesMatcher, coreConstructorMatcher, distribNot, distribNotAt, distribNotAux, distribNotOnceAt, elabConfig, finishingConstructorMatcher, tauto, tautoCore, tautology, tautoToGrind, tautoToGrind, tautoToGrind, tautoToGrindRegressions	18
Theorems	0
Total	18

Mathlib.Tactic.Tauto

Definitions

Name	Category	Theorems
DistribNotState 📖	CompData	—
casesMatcher 📖	CompOp	—
coreConstructorMatcher 📖	CompOp	—
distribNot 📖	CompOp	—
distribNotAt 📖	CompOp	—
distribNotAux 📖	CompOp	—
distribNotOnceAt 📖	CompOp	—
elabConfig 📖	CompOp	—
finishingConstructorMatcher 📖	CompOp	—
tauto 📖	CompOp	—
tautoCore 📖	CompOp	—
tautology 📖	CompOp	—

Mathlib.Tactic.Tauto.DistribNotState

Definitions

Name	Category	Theorems
currentGoal 📖	CompOp	—
fvars 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
tautoToGrind 📖	CompOp	—
tautoToGrindRegressions 📖	CompOp	—

linter.tacticAnalysis

Definitions

Name	Category	Theorems
tautoToGrind 📖	CompOp	—

linter.tacticAnalysis.regressions

Definitions

Name	Category	Theorems
tautoToGrind 📖	CompOp	—

---

← Back to Index