import everything

Stream: general

[Kenny Lau]

should / do we have a test file that imports every file?

[Simon Hudon]

Why?

[Kenny Lau]

to test for conflict?

[Simon Hudon]

You mean declarations with the same name?

[Kenny Lau]

right

[Simon Hudon]

This is what

        - lean --recursive --export=mathlib.txt src/
        - leanchecker mathlib.txt

accomplishes

[Kenny Lau]

oh, neat

[Simon Hudon]

Travis does it every time and you can get git to check it when you commit or push a branch

[Simon Hudon]

Or, if you know how to build a VS Code feature, you can create a command to run exactly that