mathlib
9b086e10 - chore(*): reduce imports (#3235)

Commit
5 years ago
chore(*): reduce imports (#3235) The RFC pull request simply removes some `import tactic` or `import tactic.basic`, and then makes the necessary changes in later files to import things as needed. I'm not sure if it's useful or not Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Author
Parents
Loading