Def Batteries.Tactic.Lint.structureInType

Modification history

2025-12-05 11:03
Mathlib/Tactic/Linter/Lint.lean
chore(Tactic/Linters): remove `public section` (#31803) …
Deleted Batteries.Tactic.Lint.structureInTypeView on Github →
2024-09-25 00:50
Mathlib/Tactic/Linter/Lint.lean
chore: bump dependencies and adapt to updated namespaces (#17117)
Added Batteries.Tactic.Lint.structureInTypeView on Github →