-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(*): only import one file per line #2470
Conversation
This already works in Lean 3.9: import tactic.localized
open_locale classical |
Nevertheless, I'm a fan of this idea. |
Okay, that's hopefully it. |
Good suggestion. I've done this now. |
You can merge this once the conflicts are fixed. |
bors merge |
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>
Pull request successfully merged into master. Build succeeded: |
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>
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>
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>
This perhaps-unnecessarily-obsessive PR puts every import statement on its own line.
Why?
import X
if we enforced this, it would be easier deal with commands after imports, etc.(irrelevant in 3.9)