Commit 2024-06-24 00:49 62fdad82

View on Github →

feat(lint-style): rewrite the linter for plain string adaptation notes in Lean (#14058) In true fashion, the linter (correctly) flags itself; we add these to the nolints file.

Estimated changes