UnusedTacticExtension

📁 Source: Mathlib/Tactic/Linter/UnusedTacticExtension.lean

Statistics

Metric	Count
Definitions allowedRef, allowedUnusedTacticExt, «command#allow_unused_tactic!___», «command#show_kind_»	4
Theorems	0
Total	4

Mathlib.Linter.UnusedTactic

Definitions

Name	Category	Theorems
allowedRef 📖	CompOp	—
allowedUnusedTacticExt 📖	CompOp	—
«command#allow_unused_tactic!___» 📖	CompOp	—
«command#show_kind_» 📖	CompOp	—

---

← Back to Index