mathlib3
d6d3d61e - feat(tactic/lint): add a linter for `[fintype _]` assumptions (#15202)

Commit

3 years ago

feat(tactic/lint): add a linter for `[fintype _]` assumptions (#15202) Adopted from the `decidable` linter.

Author

urkud

Parents