Def Mathlib.Linter.Style.getSetOptionMaxHeartbeatsComment

Modification history

2025-11-18 10:56
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
chore: bump toolchain to v4.26.0-rc1 (#31763)
Modified Mathlib.Linter.Style.getSetOptionMaxHeartbeatsCommentView on Github →
2025-04-10 03:41
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
feat(maxHeartbeats linter): `maxHeartbeats` require a comment (#23816) …
Added Mathlib.Linter.Style.getSetOptionMaxHeartbeatsCommentView on Github →