mathlib
591a0a00 - chore(*): only import one file per line (#2470)

Commit
5 years ago
chore(*): only import one file per line (#2470) This perhaps-unnecessarily-obsessive PR puts every import statement on its own line. Why? 1. it's nice to be able to grep for `import X` 2. ~~if we enforced this, it would be easier deal with commands after imports, etc.~~ (irrelevant in 3.9) 3. it means I can remove all unnecessary transitive imports with a script 4. it's just tidier. :-) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading