DeprecatedSyntaxLinter
📁 Source: Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
Statistics
| Metric | Count |
|---|---|
| 5 | |
| Theorems | 0 |
| Total | 5 |
Mathlib.Linter.Style.linter.style
Definitions
| Name | Category | Theorems |
|---|---|---|
admit 📖 | CompOp | — |
induction 📖 | CompOp | — |
maxHeartbeats 📖 | CompOp | — |
nativeDecide 📖 | CompOp | — |
refine 📖 | CompOp | — |
---