Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-17 07:06 8f6fd1b6

View on Github →

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)

Estimated changes