chore: add test for simultaneous 'import Lean' and 'import Std' (#673)

* chore: add test for simultaneous 'import Lean' and 'import Std'

* omit from prohibition on importing Lean

* CI didn't run?

* fix

Author: kim-em

.github/workflows/build.yml

@@ -67,4 +67,4 @@ jobs:
       - name: Don't 'import Lean', use precise imports
         if: always()
         run: |
-          ! (find . -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')
+          ! (find . -name "*.lean" ! -path "./test/import_lean.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

test/import_lean.lean

@@ -0,0 +1,6 @@
+import Lean
+import Std
+
+/-!
+This file ensures that we can import all of `Lean` and `Std` without name conflicts.
+-/