Linters for Mathlib #
In this file we define additional linters for mathlib.
Perhaps these should be moved to Std in the future.
Linter that checks whether a structure should be in Prop.
Mathlib.Tactic.Lint
In this file we define additional linters for mathlib.
Perhaps these should be moved to Std in the future.
Linter that checks whether a structure should be in Prop.