Naming files in test

Stream: mathlib4

[Martin Dvořák]

Are files in test supposed to be named in PascalCase, camelCase, or snake_case?

[Jon Eugster]

I think PascalCase would make the most sense.

But so far I believe there's been no rule, and certainly none that would have been enforced. Also, might not have been important enough to ever rename test files to match any uniform style

[Kim Morrison]

If someone would like to change the test directory to MathlibTest, and set it up as a lean_lib with @[testDriver] attribute (e.g. like Aesop already does), that would be great. This would allow test files importing other test files, and remove our reliance on the current ad hoc test driver script.