Def Mathlib.Linter.Style.getSetOptionMaxHeartbeatsComment

Modification history

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 →