mathlib3
8f6fd1b6 - lint(*): curly braces linter (#10280)

Commit
4 years ago
lint(*): curly braces linter (#10280) This PR: 1. Adds a style linter for curly braces: a line shall never end with `{` or start with `}` (modulo white space) 2. Adds `scripts/cleanup-braces.{sh,py}` to reflow lines that violate (1) 3. Runs the scripts from (2) to generate a boatload of changes in mathlib 4. Fixes one line that became to long due to (3)
Author
Parents
Loading