Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-17 18:30 fefdcf52

View on Github →

feat(tactic/lint): add universe linter (#8685)

  • The linter checks that there are no bad max u v occurrences in declarations (bad means that neither u nor v occur by themselves). See documentation for more details.
  • meta/expr now imports meta/rb_map (but this doesn't give any new transitive imports, so it barely matters). I also removed a transitive import from meta/rb_map.

Estimated changes